aboutsummaryrefslogtreecommitdiffhomepage
path: root/configure
diff options
context:
space:
mode:
authorGravatar coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-01-29 14:49:44 +0000
committerGravatar coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-01-29 14:49:44 +0000
commit29c33c1143635d89b82048835082c133439fffbd (patch)
tree39324d085b47c3613ed5a55cb559a362c0a07fe8 /configure
parentd6997b13582a19772a74fc5b198fa3752d9e2b16 (diff)
pour ide sous windows
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5267 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'configure')
-rwxr-xr-xconfigure14
1 files changed, 8 insertions, 6 deletions
diff --git a/configure b/configure
index df49e5d12..689cd4804 100755
--- a/configure
+++ b/configure
@@ -389,12 +389,14 @@ echo ""
rm -f $COQTOP/config/Makefile
-#case $ARCH in
-# win32)
-# BINDIR=`echo $BINDIR |sed -e 's|\\\|/|g'`
-# LIBDIR=`echo $LIBDIR |sed -e 's|\\\|/|g'`
-# MANDIR=`echo $MANDIR |sed -e 's|\\\|/|g'`;;
-#esac
+case $ARCH in
+ win32)
+ BINDIR=`echo $BINDIR |sed -e 's|\\\|/|g'`
+ LIBDIR=`echo $LIBDIR |sed -e 's|\\\|/|g'`
+ MANDIR=`echo $MANDIR |sed -e 's|\\\|/|g'`
+ EMACSLIB=`echo $EMACSLIB |sed -e 's|\\\|/|g'`
+ ;;
+esac
sed -e "s|LOCALINSTALLATION|$local|" \
-e "s|COQTOPDIRECTORY|$COQTOP|" \