aboutsummaryrefslogtreecommitdiffhomepage
path: root/configure.ml
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2017-01-12 14:03:47 +0100
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2017-01-12 14:03:47 +0100
commit5391d15256af65a0ba0ead4ee6d1ec16f7e362cc (patch)
treeb91db7d25a47898163243957d86a2d259b853866 /configure.ml
parent11bdfe88061c5bda160baec625b862a146809024 (diff)
Fix configure crash on some version strings of camlp5, e.g. "6.18-exp" (bug #5307).
Diffstat (limited to 'configure.ml')
-rw-r--r--configure.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/configure.ml b/configure.ml
index 42c2e2785..04b04979d 100644
--- a/configure.ml
+++ b/configure.ml
@@ -563,7 +563,7 @@ let check_camlp5 testcma = match !Prefs.camlp5dir with
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
+ match numeric_prefix_list version with
| 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 < 6.06 or unrecognized).\n"