aboutsummaryrefslogtreecommitdiffhomepage
path: root/configure.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-05-02 08:03:05 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-05-02 08:03:05 +0200
commit97adfc372fd716c6701677b69950cd9279f46f27 (patch)
tree0f0b23f778074065d8920a9c55db81d36d854833 /configure.ml
parent54277abbf0fa15e0437d2a68859ceeef09ec70c3 (diff)
parentbd5da52c6c625cb4559dd92051384383473ecb1b (diff)
Merge branch 'v8.5'
Diffstat (limited to 'configure.ml')
-rw-r--r--configure.ml9
1 files changed, 5 insertions, 4 deletions
diff --git a/configure.ml b/configure.ml
index 80a776471..5baaf6d8c 100644
--- a/configure.ml
+++ b/configure.ml
@@ -566,10 +566,11 @@ let check_camlp5_version () =
| _ -> die "Error: unsupported Camlp5 (version < 5.01 or unrecognized).\n"
let check_caml_version_for_camlp4 () =
- if caml_version_nums = [4;1;0] && !Prefs.debug then
- die ("Your version of OCaml is 4.01.0 which fails to compile Coq in -debug\n" ^
- "mode with Camlp4. Remove -debug option or use a different version of OCaml\n" ^
- "or use Camlp5.\n")
+ if caml_version_nums = [4;1;0] && !Prefs.debug && not !Prefs.force_caml_version then
+ die ("Your version of OCaml is detected to be 4.01.0 which fails to compile\n" ^
+ "Coq in -debug mode with Camlp4. Remove -debug option or use a different\n" ^
+ "version of OCaml or use Camlp5, or bypass this test by using option\n" ^
+ "-force-caml-version.\n")
let config_camlpX () =
try