Closed reiniscirpons closed 2 months ago
As an aside, what is the --open
parameter used for in the script? I thought it was a flag which would open the overall coverage index.html
my browser, but it seems like it takes a file and outputs a link to the specific coverage for that file (with a specific reference to a missing line if the coverage contains a missed line).
Thanks @reiniscirpons
This PR fixes the GAP coverage script on certain platforms. The issue seems to be caused by feeding raw
\n
newlines intogap
, as a fix we add non-raw newlines after the_GAP_COMMANDS
are created.Once accepted, these changes should also be propagated to the
Digraphs
package, since it uses an identical script.