blob: 7900c034da25a17492e328341edb7394dfffb198 (
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.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'
|
