aboutsummaryrefslogtreecommitdiffhomepage
path: root/configure.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2016-06-20 15:41:16 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2016-06-20 15:41:16 +0200
commit6c34cc04f5bf58973bfa1f5626b8f989a42da97c (patch)
tree55a99c3353a3ef2f0898307b51325098e4ee5b54 /configure.ml
parentbef8d3ec1c1ea37b6867519fa7c9da80ccd6b3f6 (diff)
parent058209a96579c73d786a3ceb8a7445cd5b7a8962 (diff)
Merge remote-tracking branch 'github/pr/212' into trunk
Diffstat (limited to 'configure.ml')
-rw-r--r--configure.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/configure.ml b/configure.ml
index 2e7bf1854..a1c243d65 100644
--- a/configure.ml
+++ b/configure.ml
@@ -550,9 +550,9 @@ let check_camlp5_version camlp5o =
let version_line, _ = run ~err:StdOut camlp5o ["-v"] in
let version = List.nth (string_split ' ' version_line) 2 in
match string_split '.' version with
- | major::minor::_ when s2i major > 5 || (s2i major, s2i minor) >= (5,1) ->
+ | major::minor::_ when s2i major > 6 || (s2i major, s2i minor) >= (6,6) ->
printf "You have Camlp5 %s. Good!\n" version; version
- | _ -> die "Error: unsupported Camlp5 (version < 5.01 or unrecognized).\n"
+ | _ -> die "Error: unsupported Camlp5 (version < 6.06 or unrecognized).\n"
let check_caml_version_for_camlp4 () =
if caml_version_nums = [4;1;0] && !Prefs.debug && not !Prefs.force_caml_version then