diff options
| author | Hugo Herbelin | 2020-05-18 18:15:27 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-05-18 18:15:27 +0200 |
| commit | 2222e455f0501b700f198ab614d8743229062f73 (patch) | |
| tree | ccdb912bdc17be6929cc41d95dd7a894d5c3d2d3 /test-suite/Makefile | |
| parent | ea6cb6b542e8c356192bb77f234586e0f6d55c8c (diff) | |
| parent | 3decaca622bd0005c861000529c9b006f1b6a7d7 (diff) | |
Merge PR #12289: test-suite: fix bug causing unit tests to be skipped
Reviewed-by: herbelin
Diffstat (limited to 'test-suite/Makefile')
| -rw-r--r-- | test-suite/Makefile | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index bbd31486fe..f0f838680e 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -281,8 +281,8 @@ OCAMLOPT := $(OCAMLFIND) opt $(CAMLFLAGS) OCAMLC := $(OCAMLFIND) ocamlc $(CAMLFLAGS) # ML files from unit-test framework, not containing tests -UNIT_SRCFILES:=$(shell find ./unit-tests/src -name *.ml) -UNIT_ALLMLFILES:=$(shell find ./unit-tests -name *.ml) +UNIT_SRCFILES:=$(shell find ./unit-tests/src -name '*.ml') +UNIT_ALLMLFILES:=$(shell find ./unit-tests -name '*.ml') UNIT_MLFILES:=$(filter-out $(UNIT_SRCFILES),$(UNIT_ALLMLFILES)) UNIT_LOGFILES:=$(patsubst %.ml,%.ml.log,$(UNIT_MLFILES)) @@ -312,11 +312,6 @@ unit-tests/%.ml.log: unit-tests/%.ml unit-tests/src/$(UNIT_LINK) $(HIDE)$(OCAMLBEST) -linkall -linkpkg -package coq.toplevel,oUnit \ -I unit-tests/src $(UNIT_LINK) $< -o $<.test; $(HIDE)./$<.test -unit-tests/ide/%.ml.log: unit-tests/ide/%.ml unit-tests/src/$(UNIT_LINK) - $(SHOW) 'TEST $<' - $(HIDE)$(OCAMLBEST) -linkall -linkpkg -package coq.ide,oUnit \ - -I unit-tests/src $(UNIT_LINK) $< -o $<.test; - $(HIDE)./$<.test ####################################################################### # Other generic tests |