diff options
Diffstat (limited to 'configure.ml')
| -rw-r--r-- | configure.ml | 19 |
1 files changed, 6 insertions, 13 deletions
diff --git a/configure.ml b/configure.ml index a3644982c..06a7dd822 100644 --- a/configure.ml +++ b/configure.ml @@ -767,14 +767,16 @@ let check_lablgtk_version src dir = match src with let v, _ = tryrun camlexec.find ["query"; "-format"; "%v"; "lablgtk2"] in try let vi = List.map s2i (numeric_prefix_list v) in - if vi = [2; 18; 0] then + if vi < [2; 16; 0] then + (false, v) + else if vi < [2; 18; 3] then begin - (* Version 2.18.3 is known to report incorrectly as 2.18.0 *) - printf "Warning: could not check the version of lablgtk2.\nMake sure your version is at least 2.18.3.\n"; + (* Version 2.18.3 is known to report incorrectly as 2.18.0, and Launchpad packages report as version 2.16.0 due to a misconfigured META file; see https://bugs.launchpad.net/ubuntu/+source/lablgtk2/+bug/1577236 *) + printf "Warning: Your installed lablgtk reports as %s.\n It is possible that the installed version is actually more recent\n but reports an incorrect version. If the installed version is\n actually more recent than 2.18.3, that's fine; if it is not,\n CoqIDE will compile but may be very unstable.\n" v; (true, "an unknown version") end else - ([2; 18; 3] <= vi, v) + (true, v) with _ -> (false, v) let pr_ide = function No -> "no" | Byte -> "only bytecode" | Opt -> "native" @@ -864,13 +866,6 @@ let strip = if strip = "" then "strip" else strip end -(** * md5sum command *) - -let md5sum = - select_command "Don’t know how to compute MD5 checksums…" [ - "md5sum", [], [ "--version" ]; - "md5", ["-q"], [ "-s" ; "''" ]; - ] (** * Documentation : do we have latex, hevea, ... *) @@ -1249,8 +1244,6 @@ let write_makefile f = pr "# Unix systems and profiling: true\n"; pr "# Unix systems and no profiling: strip\n"; pr "STRIP=%s\n\n" strip; - pr "#the command md5sum\n"; - pr "MD5SUM=%s\n\n" md5sum; pr "# LablGTK\n"; pr "COQIDEINCLUDES=%s\n\n" !lablgtkincludes; pr "# CoqIde (no/byte/opt)\n"; |