aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rwxr-xr-xconfigure2
1 files changed, 1 insertions, 1 deletions
diff --git a/configure b/configure
index 87b773f37..d7a86d04d 100755
--- a/configure
+++ b/configure
@@ -630,7 +630,7 @@ else
if [ "$lablgtkdir" = "" ]; then
echo "LablGtk2 not found: CoqIde will not be available."
COQIDE=no
- elif [ -z "`grep -w convert_with_fallback "$lablgtkdir/glib.mli"`" ]; then
+ elif [ -z "`grep -w Windowing "$lablgtkdir/gdk.mli"`" ]; then
echo "LablGtk2 found but too old: CoqIde will not be available."
COQIDE=no;
elif [ "$coqide_spec" = "yes" -a "$COQIDE" = "byte" ]; then