aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqtop.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/coqtop.ml')
-rw-r--r--toplevel/coqtop.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 2fa9f0ab4..437b7b0ac 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -727,9 +727,9 @@ let parse_args arglist =
|"-noinit"|"-nois" -> load_init := false
|"-no-glob"|"-noglob" -> Dumpglob.noglob (); glob_opt := true
|"-native-compiler" ->
- if Coq_config.no_native_compiler then
+ if not Coq_config.native_compiler then
warning "Native compilation was disabled at configure time."
- else Flags.native_compiler := true
+ else Flags.output_native_objects := true
|"-output-context" -> output_context := true
|"-profile-ltac" -> Flags.profile_ltac := true
|"-q" -> Coqinit.no_load_rc ()