blob: 729de2f366b167da442527f598501647207cea2d (
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.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'
|
