diff options
| author | Enrico Tassi | 2020-09-17 13:08:03 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2020-09-17 13:08:03 +0200 |
| commit | 09a8989d98219e974ceb7a2620686117c9ad6fef (patch) | |
| tree | 1428916ae8266061a29a14badf5af3c993fd6891 /.gitlab-ci.yml | |
| parent | 090550218d0a6d08c7df34b1238d5c0d38520bd5 (diff) | |
[ci] call dmesg after quick/async jobs to detect OOM
Diffstat (limited to '.gitlab-ci.yml')
| -rw-r--r-- | .gitlab-ci.yml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index ca5584bcb5..1f0c24c38b 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -325,6 +325,8 @@ build:base+async: variables: COQ_EXTRA_CONF: "-native-compiler yes -coqide opt" COQUSERFLAGS: "-async-proofs on" + after_script: + - dmesg timeout: 100m allow_failure: true # See https://github.com/coq/coq/issues/9658 only: @@ -336,6 +338,8 @@ build:quick: variables: COQ_EXTRA_CONF: "-native-compiler no" QUICK: "1" + after_script: + - dmesg timeout: 100m allow_failure: true # See https://github.com/coq/coq/issues/9637 only: |