| Age | Commit message (Collapse) | Author |
|---|
|
By running `make -k; make` whenever `make` initially fails, we can get
error messages to occur at the end of the log. This way they'll show up
on the GitHub Actions preview/summary, rather than me having to go
digging for them in the GitLab logs.
|
|
The current `perf` CI target is quite heavy, failing from out of
memory sometimes. We use the target suggested by Jason Gross (<- thanks)
in https://github.com/coq/coq/pull/12577#issuecomment-651970064
|
|
It's tested on the bench, so might as well test it on the CI. Hopefully
it's not too memory-heavy. (It should only take a couple of minutes,
time-wise.)
|
