aboutsummaryrefslogtreecommitdiffhomepage
path: root/configure.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-01-17 15:22:36 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-01-17 15:22:36 +0100
commit4d8903c06fd9fd2aca793da8bb55448906347a8c (patch)
tree132b1119a9c95abecc81387733d2900eaf55f838 /configure.ml
parentcccf7d618bc85fb5158b98bbf967bbc1c9bdc576 (diff)
parentd034d8359512b509788a5c08de153b1ade670d66 (diff)
Merge PR #6600: Update configure.ml to only warn on lablgtk >= 2.16.0 and < 2.18.3
Diffstat (limited to 'configure.ml')
-rw-r--r--configure.ml10
1 files changed, 6 insertions, 4 deletions
diff --git a/configure.ml b/configure.ml
index ff767d96b..b5de5e3e1 100644
--- a/configure.ml
+++ b/configure.ml
@@ -764,14 +764,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"