diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-04-24 15:33:09 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-04-24 15:45:23 +0200 |
| commit | 65578a55b81252e2c4b006728522839a9e37cd5c (patch) | |
| tree | 3483e373cb116211e00ee664dea78efe874d39ec /configure.ml | |
| parent | fd13e21ccb89e2fa3a80074f9d7afd8b0638fdcb (diff) | |
| parent | 96bb190caa138c91b4d5e5f96d6f179811a177c8 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'configure.ml')
| -rw-r--r-- | configure.ml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/configure.ml b/configure.ml index b8bb650b1..80a776471 100644 --- a/configure.ml +++ b/configure.ml @@ -565,6 +565,12 @@ let check_camlp5_version () = | Not_found -> die "Error: cannot find Camlp5 binaries in path.\n" | _ -> 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") + let config_camlpX () = try if not !Prefs.usecamlp5 then raise NoCamlp5; @@ -583,6 +589,7 @@ let config_camlpX () = let camlp4orf = which_camlpX "camlp4orf" in let version_line, _ = run ~err:StdOut camlp4orf ["-v"] in let camlp4_version = List.nth (string_split ' ' version_line) 2 in + check_caml_version_for_camlp4 (); "camlp4", camlp4orf, Filename.dirname camlp4orf, camlp4libdir, camlp4mod, camlp4_version with _ -> die "No Camlp4 installation found.\n" |