aboutsummaryrefslogtreecommitdiff
path: root/Makefile.build
diff options
context:
space:
mode:
authorHugo Herbelin2015-05-15 11:37:43 +0200
committerHugo Herbelin2015-05-15 11:39:49 +0200
commit5d015ae0d90fd7fd3d440acee6ccd501d8b63ba0 (patch)
treee73fb685fea3bd4aa5a9eecde1df69c518acccf0 /Makefile.build
parent76c3b40482978fffca50f6f59e8bcae455680aba (diff)
parent3fb81febe8efc34860688cac88a2267cfe298cf7 (diff)
Merge v8.5 into trunk
Conflicts: tactics/eauto.ml4 (merging eauto.ml4 and adapting coq_micromega.ml to new typing.ml API)
Diffstat (limited to 'Makefile.build')
-rw-r--r--Makefile.build2
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