From 4ad6855504db2ce15a474bd646e19151aa8142e2 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 14 May 2015 09:53:36 +0200
Subject: Disable precompilation for native_compute by default.

Note that this does not prevent using native_compute, but it will force
on-the-fly recompilation of dependencies whenever it is used.

Precompilation is enabled for the standard library, assuming native
compilation was enabled at configuration time.

If native compilation was disabled at configuration time, native_compute
falls back to vm_compute.

Failure to precompile is a hard error, since it is now explicitly required
by the user.
---
 Makefile.build | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Makefile.build')

diff --git a/Makefile.build b/Makefile.build
index 018471b684..41220792d5 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 
-- 
cgit v1.2.3