diff options
| author | Gereon Kremer <nafur42@gmail.com> | 2021-11-05 18:05:58 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-11-06 01:05:58 +0000 |
| commit | 733ab2f6b9430b2ae5824e2614de5811a60033f3 (patch) | |
| tree | 87385312209266de9c73d4a4ed4c35690c1945e2 /src/theory/quantifiers/quantifiers_rewriter.h | |
| parent | 1909b36e01578099d7a773e561b4bec15c067580 (diff) | |
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.
Diffstat (limited to 'src/theory/quantifiers/quantifiers_rewriter.h')
0 files changed, 0 insertions, 0 deletions