diff options
| author | Hugo Herbelin | 2018-12-09 20:33:46 +0100 |
|---|---|---|
| committer | Vincent Laporte | 2019-03-19 08:40:17 +0000 |
| commit | f3ccaf7b094bce98b309263aac862413bbb86b2d (patch) | |
| tree | 5b2d15dbb16308a8e3475864cb67e0c6ca877cbc /configure.ml | |
| parent | 238d83080c8dbed458b026c93f5c723c1bd7c937 (diff) | |
Configuration: expand a version number to three fields when only 1 or 2 fields are given.
Diffstat (limited to 'configure.ml')
| -rw-r--r-- | configure.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/configure.ml b/configure.ml index 8b6fccb5e3..266abdf3b9 100644 --- a/configure.ml +++ b/configure.ml @@ -150,7 +150,10 @@ let numeric_prefix_list s = let max = String.length s in let i = ref 0 in while !i < max && isnum s.[!i] do incr i done; - string_split '.' (String.sub s 0 !i) + match string_split '.' (String.sub s 0 !i) with + | [v] -> [v;"0";"0"] + | [v1;v2] -> [v1;v2;"0"] + | v -> v (** Combined existence and directory tests *) |