diff options
| author | Gaëtan Gilbert | 2020-05-18 11:17:13 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-05-18 11:20:09 +0200 |
| commit | 835289d50aec9172db49e2c4849ad1f73a1d36b3 (patch) | |
| tree | 18407634cb37e18752300de475a41775a4cf4f02 | |
| parent | b9591f15d75886456ff28984934de73d6a516af5 (diff) | |
test-suite/Makefile: fix incomplete prerequisite list
| -rw-r--r-- | test-suite/Makefile | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index dece21885c..bbd31486fe 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -117,10 +117,7 @@ VSUBSYSTEMS := prerequisite success failure $(BUGS) output output-coqtop \ # All subsystems SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile tools $(UNIT_TESTS) -PREREQUISITELOG = prerequisite/admit.v.log \ - prerequisite/make_local.v.log prerequisite/make_notation.v.log \ - prerequisite/bind_univs.v.log prerequisite/module_bug8416.v.log \ - prerequisite/module_bug7192.v.log +PREREQUISITELOG = $(addsuffix .log,$(wildcard prerequisite/*.v)) ####################################################################### # Phony targets |