diff options
| author | filliatr | 2003-05-19 10:56:47 +0000 |
|---|---|---|
| committer | filliatr | 2003-05-19 10:56:47 +0000 |
| commit | ca3bc1725eac3b17fe26be50ea506318d5983984 (patch) | |
| tree | 22955a9491164933e62a12ff9a5e324877352df9 /configure | |
| parent | de2dee71b9c2ed3f001ca825766ae600955a31d4 (diff) | |
configure et make install s'occupent de CoqIde tout seuls
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4029 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'configure')
| -rwxr-xr-x | configure | 24 |
1 files changed, 23 insertions, 1 deletions
@@ -39,6 +39,7 @@ emacs_spec=no reals_opt=no reals=all arch_spec=no +coqide_spec=no COQTOP=`pwd` @@ -92,6 +93,9 @@ while : ; do -reals|--reals) reals_opt=yes reals=$2 shift;; + -coqide|--coqide) coqide_spec=yes + COQIDE=$2 + shift;; -byte-only|-byteonly|--byteonly|--byte-only) best_compiler=byte;; -debug|--debug) coq_debug_flag=-g;; -profile|--profile) coq_profile_flag=-p;; @@ -310,7 +314,23 @@ case $OS in *) CAMLP4LIB=${CAMLLIB}/camlp4 esac - + +# lablgtk2 and CoqIDE + +if test $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 + fi +else + COQIDE=no +fi +fi + # Tell on windows if ocaml understands cygwin or windows path formats "$CAMLC" -o config/giveostype config/giveostype.ml @@ -346,6 +366,7 @@ echo " Reals theory : All" else echo " Reals theory : Basic" fi +echo " CoqIde : $COQIDE" echo "" echo " Paths for true installation:" @@ -389,6 +410,7 @@ sed -e "s|LOCALINSTALLATION|$local|" \ -e "s|NATIVECAMLC|$nativecamlc|" \ -e "s|STRIPCOMMAND|$STRIPCOMMAND|" \ -e "s|REALSOPT|$reals|" \ + -e "s|COQIDEOPT|$COQIDE|" \ $COQTOP/config/Makefile.template > $COQTOP/config/Makefile chmod a-w $COQTOP/config/Makefile |