diff options
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.build b/Makefile.build index 8f64d1ff26..a790b92b2e 100644 --- a/Makefile.build +++ b/Makefile.build @@ -81,7 +81,7 @@ TIMECMD= # if you prefer a specific time command instead of $(STDTIME) STDTIME=/usr/bin/time -f "$* (user: %U mem: %M ko)" TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) -COQOPTS=$(COQ_XML) $(VM) +COQOPTS=$(COQ_XML) $(VM) $(NATIVECOMPUTE) BOOTCOQC=$(TIMER) $(COQTOPEXE) -boot $(COQOPTS) -compile # The SHOW and HIDE variables control whether make will echo complete commands |