You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Using --depth=1 like that is very problematic, because, well, we discard all history -- so of course it can't really merge it. To fix this, it probably suffices to get rid of all --depth arguments to git. And of course switching to a release version of GAP like 4.10.2, would also get rid of this problem.
Merging PR #272 and rebuilding GAP
caused the following error:
I worked around it by invoking
in
~/.julia/dev/GAP/gap
.The text was updated successfully, but these errors were encountered: