diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-19 13:17:08 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-19 13:20:21 +0200 |
| commit | fa1e921257735d246d04be9e456f11ec7330b37a (patch) | |
| tree | 2b857e5147e2b9e7b42997ad90f483e67d809593 /test-suite/Makefile | |
| parent | 9f11adda4bff194a3c6a66d573ce7001d4399886 (diff) | |
Re-adding explicit dependency of misc universe test into all_stdlib.v.
Was working when calling test-suite from main Makefile but not when
calling directly from the test-suite Makefile.
The dependency was mistakenly dropped in 98a927aef.
Diffstat (limited to 'test-suite/Makefile')
| -rw-r--r-- | test-suite/Makefile | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 39ef05269..afaa48463 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -408,6 +408,11 @@ modules/%.vo: modules/%.v misc: $(patsubst %.sh,%.log,$(wildcard misc/*.sh)) +misc/universes.log: misc/universes/all_stdlib.v + +misc/universes/all_stdlib.v: + cd .. && $(MAKE) test-suite/$@ + $(patsubst %.sh,%.log,$(wildcard misc/*.sh)): %.log: %.sh $(PREREQUISITELOG) @echo "TEST $<" $(HIDE){ \ |