aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorChantal Keller <Chantal.Keller@inria.fr>2020-03-25 18:46:08 +0100
committerChantal Keller <Chantal.Keller@inria.fr>2020-03-25 18:46:08 +0100
commita3146935a48337634f6810d53a7cc7302cb61d47 (patch)
tree146079a0559b62de3d46ed3dde362e26a375d34c
parentbaeb3e355eaa0e0dd0601c3a9265e996ea534512 (diff)
downloadsmtcoq-a3146935a48337634f6810d53a7cc7302cb61d47.tar.gz
smtcoq-a3146935a48337634f6810d53a7cc7302cb61d47.zip
make test does not need cleaning anymore
-rw-r--r--src/versions/standard/Makefile.local8
-rw-r--r--unit-tests/Makefile8
2 files changed, 10 insertions, 6 deletions
diff --git a/src/versions/standard/Makefile.local b/src/versions/standard/Makefile.local
index 045af88..089ae9a 100644
--- a/src/versions/standard/Makefile.local
+++ b/src/versions/standard/Makefile.local
@@ -5,16 +5,16 @@
test :
- cd ../unit-tests; make
+ cd ../unit-tests; make cleanvo; make
ztest :
- cd ../unit-tests; make zchaff
+ cd ../unit-tests; make cleanvo; make zchaff
vtest :
- cd ../unit-tests; make verit
+ cd ../unit-tests; make cleanvo; make verit
lfsctest :
- cd ../unit-tests; make lfsc
+ cd ../unit-tests; make cleanvo; make lfsc
clean::
cd ../unit-tests; make clean
diff --git a/unit-tests/Makefile b/unit-tests/Makefile
index 0d4bdc1..d8e9be0 100644
--- a/unit-tests/Makefile
+++ b/unit-tests/Makefile
@@ -39,5 +39,9 @@ logs: $(OBJ)
$(COQC) $(COQDEBUG) $(COQFLAGS) $*
-clean:
- rm -rf *~ $(ZCHAFFLOG) $(VERITLOG) *.vo *.glob
+clean: cleanvo
+ rm -rf *~ $(ZCHAFFLOG) $(VERITLOG)
+
+
+cleanvo:
+ rm -rf *~ *.vo *.glob