diff options
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/Makefile.build b/Makefile.build index b2b311a4f..d14152842 100644 --- a/Makefile.build +++ b/Makefile.build @@ -63,14 +63,13 @@ READABLE_ML4= # non-empty means .ml of .ml4 will be ascii instead of binary VALIDATE= COQ_XML= # is "-xml" when building XML library VM= # is "-no-vm" to not use the vm" -UNBOXEDVALUES= # is "-unboxed-values" to use unboxed values TIMECMD= # is "'time -p'" to get compilation time of .v # NB: variable TIME, if set, is the formatting string for unix command 'time'. # For instance: # TIME="%C (%U user, %S sys, %e total, %M maxres)" -COQOPTS=$(COQ_XML) $(VM) $(UNBOXEDVALUES) +COQOPTS=$(COQ_XML) $(VM) BOOTCOQTOP:=$(TIMECMD) $(BESTCOQTOP) -boot $(COQOPTS) # The SHOW and HIDE variables control whether make will echo complete commands |