blob: 7ab0bc75d9be5fbc277ab7bf8b486ae40a588ceb (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
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.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'
|
