diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-17 21:55:18 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-17 22:01:35 +0200 |
| commit | 50266aab0b9d9ba3bede37429bcdc5c2bfdc1159 (patch) | |
| tree | c3fc613efdc2ae9d58baf21a7a09df4f05654533 /configure.ml | |
| parent | f5dc54519f2a62bab2f7b9059e8c3c8dc53619be (diff) | |
Updating configure.ml wrt Coq not compilable with OCaml 4.01.0 in debug mode.
Diffstat (limited to 'configure.ml')
| -rw-r--r-- | configure.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/configure.ml b/configure.ml index 48bcf34e1..6291de03c 100644 --- a/configure.ml +++ b/configure.ml @@ -520,6 +520,9 @@ let check_caml_version () = die ("Your version of OCaml is 4.02.0 which suffers from a bug inducing\n" ^ "very slow compilation times. If you still want to use it, use \n" ^ "option -force-caml-version.\n") + else 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 mode.\nRemove -debug option or use a different version of OCaml.\n") else printf "You have OCaml %s. Good!\n" caml_version else |