diff options
author | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2017-01-12 14:03:47 +0100 |
---|---|---|
committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2017-01-12 14:03:47 +0100 |
commit | 5391d15256af65a0ba0ead4ee6d1ec16f7e362cc (patch) | |
tree | b91db7d25a47898163243957d86a2d259b853866 /configure.ml | |
parent | 11bdfe88061c5bda160baec625b862a146809024 (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.ml | 2 |
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" |