From e2e7fea91f3af5dcf62052078da65489b796e9e2 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 31 Oct 2018 11:45:09 +0100
Subject: Pass native and VM flags to the kernel through environment

The kernel no longer has to read the configure flag, its value can now
be overriden by a coqtop/coqc argument, and more generally is easier to
set from a toplevel (such as the checker).

We also add a `-bytecode-compiler` flag.

Fixes #4607
---
 tools/coqc.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'tools')

diff --git a/tools/coqc.ml b/tools/coqc.ml
index 2cbf05bd8b..ad845470ec 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -97,7 +97,7 @@ let parse_args () =
       |"-batch"|"-noinit"|"-nois"|"-noglob"|"-no-glob"
       |"-q"|"-profile"|"-echo" |"-quiet"
       |"-silent"|"-m"|"-beautify"|"-strict-implicit"
-      |"-impredicative-set"|"-vm"|"-native-compiler"
+      |"-impredicative-set"|"-vm"
       |"-indices-matter"|"-quick"|"-type-in-type"
       |"-async-proofs-always-delegate"|"-async-proofs-never-reopen-branch"
       |"-stm-debug"
@@ -111,7 +111,7 @@ let parse_args () =
       |"-load-ml-source"|"-require"|"-load-ml-object"
       |"-init-file"|"-dump-glob"|"-compat"|"-coqlib"|"-top"
       |"-async-proofs-j" |"-async-proofs-private-flags" |"-async-proofs" |"-w"
-      |"-o"|"-profile-ltac-cutoff"|"-mangle-names"
+      |"-o"|"-profile-ltac-cutoff"|"-mangle-names"|"-bytecode-compiler"|"-native-compiler"
       as o) :: rem ->
 	begin
 	  match rem with
-- 
cgit v1.2.3