From 1596cdbb2e97f2353236e35fb07be05efe6d1a84 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Wed, 11 Nov 2020 17:07:14 +0100
Subject: Configure default value of -native-compiler

This an implementation of point 2 of CEP coq/ceps#48
https://github.com/coq/ceps/pull/48

Option -native-compiler of the configure script now impacts the
default value of the option -native-compiler of coqc. The
-native-compiler option of the configure script is added an ondemand
value, which becomes the default, thus preserving the previous default
behavior.

The stdlib is still precompiled when configuring with -native-compiler
yes. It is not precompiled otherwise.
---
 config/coq_config.mli | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'config')

diff --git a/config/coq_config.mli b/config/coq_config.mli
index 12856cb6e6..809fa3d758 100644
--- a/config/coq_config.mli
+++ b/config/coq_config.mli
@@ -57,4 +57,5 @@ val wwwstdlib : string
 val localwwwrefman : string
 
 val bytecode_compiler : bool
-val native_compiler : bool
+type native_compiler = NativeOff | NativeOn of { ondemand : bool }
+val native_compiler : native_compiler
-- 
cgit v1.2.3