diff options
| author | Jason Gross | 2020-12-31 18:22:08 -0500 |
|---|---|---|
| committer | Jason Gross | 2021-01-11 22:18:44 -0500 |
| commit | 1debe206dff53dfb20795ddf40d0a328d2252a6f (patch) | |
| tree | ee3e3332f2726c3fe4bb5c2be3344d96b423ab56 /dev/ci/gitlab.bat | |
| parent | 039f04c2caf7c8da380ca8d582e9edae3e6d5c06 (diff) | |
[ci] [coq-performance-tests] Errors at end of log
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.
Diffstat (limited to 'dev/ci/gitlab.bat')
0 files changed, 0 insertions, 0 deletions