projects
/
cvc5.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
| inline |
side by side
(parent:
bdba2bf
)
Fix 'make regress' (#1683)
author
Andres Noetzli
<andres.noetzli@gmail.com>
Wed, 21 Mar 2018 23:51:56 +0000
(16:51 -0700)
committer
GitHub
<noreply@github.com>
Wed, 21 Mar 2018 23:51:56 +0000
(16:51 -0700)
Commit
b8db52f9bad5b1053810c93f0067de8423349da3
removed the option to do "make regress" (I only tested with "make regressX" and "make check"). This commit reenables "make regress".
test/regress/Makefile.am
patch
|
blob
|
history
diff --git
a/test/regress/Makefile.am
b/test/regress/Makefile.am
index cd245f3e6e26542dbd756345e3803d5ffdc42c4f..e1a3d7e7f4a261c9a32a51be1868c821ed483d8b 100644
(file)
--- a/
test/regress/Makefile.am
+++ b/
test/regress/Makefile.am
@@
-22,7
+22,9
@@
endif
MAKEFLAGS = -k
export VERBOSE = 1
-.PHONY: regress0 regress1 regress2 regress3 regress4
+.PHONY: regress regress0 regress1 regress2 regress3 regress4
+
+regress: regress1
regress0:
REGRESSION_LEVEL=0 $(MAKE) check