diff options
| author | Masaya Tojo <masaya@tojo.tokyo> | 2021-02-03 09:48:38 +0900 |
|---|---|---|
| committer | Masaya Tojo <masaya@tojo.tokyo> | 2021-02-03 09:48:38 +0900 |
| commit | 14f1d7683cf47db9ffd63ecbddc936d85d060581 (patch) | |
| tree | d8d016c3c0d67ded03692968df247c5f880b3058 /.gitlab-ci.yml | |
| parent | 93f5eea5de6e27c215a230575294e589dcb8f335 (diff) | |
Update CI settings
Diffstat (limited to '.gitlab-ci.yml')
| -rw-r--r-- | .gitlab-ci.yml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 4ba0910..8354564 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -12,5 +12,5 @@ test: echo '(setf sb-ext:*invoke-debugger-hook* (lambda (c h) (declare (ignore c h)) (sb-ext:quit)))' echo '(lp)' cat "$source" - } | acl2 | awk '{ print } ; $0 == "******** FAILED ********" { exit 1 }' + } | acl2 | awk '{ print } ; $0 == "******** FAILED ********" || $0 == "ACL2 !>ACL2 !>Bye." { exit 1 }' done |