diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2020-08-24 11:54:18 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-08-24 13:54:18 -0500 |
commit | 706dbdac95131bf45efbfcb9a8ca4df9dfb85478 (patch) | |
tree | 9cc6861532e486245a7362faabe7fe36d1efc4bb /.github | |
parent | 6d53928cd9f16385d81124916311c372ec20b5ed (diff) |
Increase regress level to 2 for production build. (#4888)
Diffstat (limited to '.github')
-rw-r--r-- | .github/workflows/ci.yml | 6 |
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 |