diff options
| author | Maxime Dénès | 2017-12-18 15:57:33 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-12-18 15:57:33 +0100 |
| commit | b6e05e2944c2a7976c4ac1f51694b175f52dbaf8 (patch) | |
| tree | 06cd44b057b6608823979bfbd89edd4636855a17 /test-suite | |
| parent | f27fa07029475f2366e101cff7bc895aac415b67 (diff) | |
| parent | 23e503c15cbb2602507e5afb95590f8bdc0af134 (diff) | |
Merge PR #6217: Do dependencies in 1 command per file class.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/coq-makefile/timing/after/time-of-build-after.log.desired | 3 | ||||
| -rw-r--r-- | test-suite/coq-makefile/timing/after/time-of-build-before.log.desired | 3 |
2 files changed, 2 insertions, 4 deletions
diff --git a/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired b/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired index 729de2f366..7900c034da 100644 --- a/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired +++ b/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired @@ -1,7 +1,6 @@ Makefile:69: warning: undefined variable '*' Makefile:204: warning: undefined variable 'DSTROOT' -COQDEP Fast.v -COQDEP Slow.v +COQDEP VFILES Makefile:69: warning: undefined variable '*' Makefile:204: warning: undefined variable 'DSTROOT' Makefile:69: warning: undefined variable '*' diff --git a/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired b/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired index b25bc3683c..7ab0bc75d9 100644 --- a/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired +++ b/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired @@ -1,7 +1,6 @@ Makefile:69: warning: undefined variable '*' Makefile:204: warning: undefined variable 'DSTROOT' -COQDEP Fast.v -COQDEP Slow.v +COQDEP VFILES Makefile:69: warning: undefined variable '*' Makefile:204: warning: undefined variable 'DSTROOT' Makefile:69: warning: undefined variable '*' |