From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- .../timing/after/time-of-build-after.log.desired | 15 +++++++++++++++ 1 file changed, 15 insertions(+) create mode 100644 test-suite/coq-makefile/timing/after/time-of-build-after.log.desired (limited to 'test-suite/coq-makefile/timing/after/time-of-build-after.log.desired') 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 new file mode 100644 index 00000000..7900c034 --- /dev/null +++ b/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired @@ -0,0 +1,15 @@ +Makefile:69: warning: undefined variable '*' +Makefile:204: warning: undefined variable 'DSTROOT' +COQDEP VFILES +Makefile:69: warning: undefined variable '*' +Makefile:204: warning: undefined variable 'DSTROOT' +Makefile:69: warning: undefined variable '*' +Makefile:204: warning: undefined variable 'DSTROOT' +Makefile:69: warning: undefined variable '*' +Makefile:204: warning: undefined variable 'DSTROOT' +COQC Slow.v +Slow (real: 0.04, user: 0.02, sys: 0.01, mem: 45512 ko) +COQC Fast.v +Fast (real: 0.41, user: 0.37, sys: 0.04, mem: 395200 ko) +Makefile:69: warning: undefined variable '*' +Makefile:204: warning: undefined variable 'DSTROOT' -- cgit v1.2.3