From 733ab2f6b9430b2ae5824e2614de5811a60033f3 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 5 Nov 2021 18:05:58 -0700 Subject: [PATCH] Only run regress0 for static build (#7592) It is surprisingly tricky to call ctest properly with multiple -LE arguments (and I actually doubt that the CI version of ctest adheres to its documentation). This PR avoid calling make check (which sets -LE regress[3-4] as a default) and calls ctest directly. --- .github/actions/run-tests/action.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/actions/run-tests/action.yml b/.github/actions/run-tests/action.yml index ba4502b95..5fddcbd36 100644 --- a/.github/actions/run-tests/action.yml +++ b/.github/actions/run-tests/action.yml @@ -21,9 +21,9 @@ runs: - name: Run CTest shell: bash run: | - make -j${{ env.num_proc }} check + make -j${{ env.num_proc }} build-tests + ctest -j${{ env.num_proc }} --output-on-failure -LE regress[${{ inputs.regressions-exclude }}] env: - ARGS: --output-on-failure -LE regress[${{ inputs.regressions-exclude }}] CVC5_REGRESSION_ARGS: --no-early-exit RUN_REGRESSION_ARGS: ${{ inputs.regressions-args }} working-directory: ${{ inputs.build-dir }} -- 2.30.2