diff options
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 '*' |