In build.jl: Only clone new GAP if gap subfolder not present #267
Conversation
Codecov Report
@@ Coverage Diff @@
## master #267 +/- ##
=======================================
Coverage 70.07% 70.07%
=======================================
Files 50 50
Lines 3262 3262
=======================================
Hits 2286 2286
Misses 976 976
|
| if isdir("gap") | ||
| ### Update the GAP clone | ||
| cd("gap") | ||
| run(`git pull --depth=1 origin master`) |
There was a problem hiding this comment.
So, what if we ever switch to building GAP point releases? Then gap won't be a git dir, right? So perhaps also check for the presence of .git?
Hm, IIRC, in the past, pulling in a shallow repo was problematic for various reasons (though this may have improved in recent git versions -- but of course we don't know if our users all have recent git versions, do we?). Also git pull --depth=N had its issues. Also note that this is slightly risky if files got renamed, possibly clashing with files we made.
I would therefore recommend that we also run something like git clean -fx or git clean -fdx (depending on whether we want to reuse the pkg dir or not... same for the downloaded packages...
Thinking further along this line, I wonder if we shouldn't do an out-of-tree build for GAP anyway?
No description provided.