aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired
blob: b25bc3683c93b7fd6a079e4b831cb9fdf420d3e3 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
Makefile:69: warning: undefined variable '*'
Makefile:204: warning: undefined variable 'DSTROOT'
COQDEP Fast.v
COQDEP Slow.v
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.40, user: 0.35, sys: 0.04, mem: 394968 ko)
COQC Fast.v
Fast (real: 0.04, user: 0.03, sys: 0.00, mem: 46564 ko)
Makefile:69: warning: undefined variable '*'
Makefile:204: warning: undefined variable 'DSTROOT'