summaryrefslogtreecommitdiff
path: root/.github
diff options
context:
space:
mode:
authorMathias Preiner <mathias.preiner@gmail.com>2020-08-24 11:54:18 -0700
committerGitHub <noreply@github.com>2020-08-24 13:54:18 -0500
commit706dbdac95131bf45efbfcb9a8ca4df9dfb85478 (patch)
tree9cc6861532e486245a7362faabe7fe36d1efc4bb /.github
parent6d53928cd9f16385d81124916311c372ec20b5ed (diff)
Increase regress level to 2 for production build. (#4888)
Diffstat (limited to '.github')
-rw-r--r--.github/workflows/ci.yml6
1 files changed, 5 insertions, 1 deletions
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 2d3586483..00fa15bc5 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -27,6 +27,7 @@ jobs:
cache-key: production
python-bindings: true
check-examples: true
+ exclude_regress: 3-4
- name: production-clang
config: production
@@ -34,16 +35,19 @@ jobs:
check-examples: true
env: CC=clang CXX=clang++
os: ubuntu-latest
+ exclude_regress: 1-4
- name: debug
config: debug --symfpu --lfsc --no-debug-symbols --editline
cache-key: debug
os: ubuntu-latest
+ exclude_regress: 1-4
- name: debug-cln
config: debug --symfpu --cln --gpl --no-debug-symbols --no-proofs
cache-key: debug-cln
os: ubuntu-latest
+ exclude_regress: 1-4
name: ${{ matrix.os }}:${{ matrix.name }}
runs-on: ${{ matrix.os }}
@@ -168,7 +172,7 @@ jobs:
- name: Run CTest
run: make -j2 check
env:
- ARGS: --output-on-failure -LE regress[1-4]
+ ARGS: --output-on-failure -LE regress[${{ matrix.exclude_regress }}]
CVC4_REGRESSION_ARGS: --no-early-exit
working-directory: build
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback