diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-20 14:24:54 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-12-15 22:37:58 +0100 |
| commit | b75018e36899e939de25509a579385967b9a7010 (patch) | |
| tree | 2d31bd9d2fef9c5e707733323f6619d205f21818 /test-suite/coq-makefile | |
| parent | f303ed9fb26797b9ec7d172fe583e7ee607ae441 (diff) | |
Do dependencies in 1 command per file class.
Diffstat (limited to 'test-suite/coq-makefile')
| -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 729de2f36..7900c034d 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 b25bc3683..7ab0bc75d 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 '*' |