aboutsummaryrefslogtreecommitdiff
path: root/configure
diff options
context:
space:
mode:
Diffstat (limited to 'configure')
-rwxr-xr-xconfigure13
1 files changed, 7 insertions, 6 deletions
diff --git a/configure b/configure
index bbd1bb32ac..eaaa62fac8 100755
--- a/configure
+++ b/configure
@@ -319,12 +319,13 @@ esac
if [ "$coqide_spec" = "no" ] ; then
if test -x ${CAMLLIB}/lablgtk2; then
- if grep -q -w convert_with_fallback ${CAMLLIB}/lablgtk2/glib.mli; then
- COQIDE=byte;
- fi
- # native threads
- if test -f ${CAMLLIB}/threads/threads.cmxa; then
- COQIDE=opt
+ if grep -q -w convert_with_fallbacks ${CAMLLIB}/lablgtk2/glib.mli; then
+ COQIDE=byte
+ # native threads
+ if test -f ${CAMLLIB}/threads/threads.cmxa; then
+ COQIDE=opt;
+ fi;
+ else COQIDE=no;
fi
else
COQIDE=no