aboutsummaryrefslogtreecommitdiff
path: root/configure
diff options
context:
space:
mode:
authorbertot2008-12-29 07:37:31 +0000
committerbertot2008-12-29 07:37:31 +0000
commit1903011fd6faf22cde837cbdd140306ea20e4a99 (patch)
tree0bbdf5e0d62f3656083ad4cc255f95c56497cea7 /configure
parentf5eb06f0d2b28fe72db12fb57458b961b9ae9d85 (diff)
compatibility with lablgtk2 version 2.12
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11722 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'configure')
-rwxr-xr-xconfigure4
1 files changed, 4 insertions, 0 deletions
diff --git a/configure b/configure
index dd37b2d365..cea82aaef4 100755
--- a/configure
+++ b/configure
@@ -1020,7 +1020,11 @@ fi
if [ ! "$COQIDE" = "no" ]; then
if grep "class view " "$lablgtkdir/gText.mli" | grep -q "\[>" ; then
+ if grep -q "?accepts_tab:bool" "$lablgtkdir/gText.mli" ; then
+ cp -f ide/undo_lablgtk_ge212.mli ide/undo.mli
+ else
cp -f ide/undo_lablgtk_ge26.mli ide/undo.mli
+ fi
else
cp -f ide/undo_lablgtk_lt26.mli ide/undo.mli
fi