summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMathias Preiner <mathias.preiner@gmail.com>2021-04-13 13:00:29 -0700
committerGitHub <noreply@github.com>2021-04-13 20:00:29 +0000
commit7bc8ebe940cf092d66265040db48c1e4b486c73f (patch)
tree65aa70b38364e392e05945cbc5a60446b30d2499
parent10308c88ae5de234eb62c08380d53d4967112ccd (diff)
ci: Use CVC5_REGRESSION_ARGS. (#6347)
-rw-r--r--.github/workflows/ci.yml2
1 files changed, 1 insertions, 1 deletions
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 6d22f9f11..f3800308b 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -188,7 +188,7 @@ jobs:
run: make -j2 check
env:
ARGS: --output-on-failure -LE regress[${{ matrix.exclude_regress }}]
- CVC4_REGRESSION_ARGS: --no-early-exit
+ CVC5_REGRESSION_ARGS: --no-early-exit
RUN_REGRESSION_ARGS: ${{ matrix.run_regression_args }}
working-directory: build
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback