diff options
| author | Pierre-Marie Pédrot | 2019-11-01 14:43:03 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-11-01 14:43:03 +0100 |
| commit | d00c0b93ec4cb5ca48a9dc2ddf2cfd2038208ee2 (patch) | |
| tree | 41badb2d2c77b530018af361543ed57ab41a5fcd /test-suite/Makefile | |
| parent | ef3a68200b3dad67f31aeb741479d2adc8ebf0d9 (diff) | |
| parent | c5ce7dfe595beaced11646e3aed7e3532a1353f0 (diff) | |
Merge PR #8642: Compiled interfaces with -vos and -vok options
Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: ejgallego
Ack-by: gares
Ack-by: maximedenes
Ack-by: ppedrot
Diffstat (limited to 'test-suite/Makefile')
| -rw-r--r-- | test-suite/Makefile | 23 |
1 files changed, 22 insertions, 1 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index c60f39231e..d9c89d7a8a 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -131,9 +131,10 @@ bugs: $(BUGS) clean: rm -f trace .nia.cache .lia.cache output/MExtraction.out + rm -f vos/Makefile vos/Makefile.conf $(SHOW) 'RM <**/*.stamp> <**/*.vo> <**/*.vio> <**/*.log> <**/*.glob>' $(HIDE)find . \( \ - -name '*.stamp' -o -name '*.vo' -o -name '*.vio' -o -name '*.log' -o -name '*.glob' \ + -name '*.stamp' -o -name '*.vo' -o -name '*.vio' -o -name '*.vos' -o -name '*.vok' -o -name '*.log' -o -name '*.glob' \ \) -exec rm -f {} + $(SHOW) 'RM <**/*.cmx> <**/*.cmi> <**/*.o> <**/*.test>' $(HIDE)find unit-tests \( \ @@ -748,3 +749,23 @@ tools/%.log : tools/%/run.sh $(FAIL); \ fi; \ ) > "$@" + +# vos/ + +vos: vos/run.log + +vos/run.log: $(wildcard vos/*.sh) $(wildcard vos/*.v) + @echo "TEST vos" + $(HIDE)(\ + export COQBIN=$(BIN);\ + cd vos && \ + bash run.sh 2>&1; \ + if [ $$? = 0 ]; then \ + echo $(log_success); \ + echo " $<...Ok"; \ + else \ + echo $(log_failure); \ + echo " $<...Error!"; \ + $(FAIL); \ + fi; \ + ) > "$@" |