diff options
author | 2001-04-19 14:45:14 +0000 | |
---|---|---|
committer | 2001-04-19 14:45:14 +0000 | |
commit | fdd1aae0c3f01f38b861fcedffa6449728fd43e0 (patch) | |
tree | a77f3d9e4bb17c43883e44600bf5921ca6b3ea4e /configure | |
parent | c8cba24511fe5f0ffc16fd2f7d7e53c9a1a3a791 (diff) |
ajout du cas win32
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1631 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'configure')
-rwxr-xr-x | configure | 8 |
1 files changed, 4 insertions, 4 deletions
@@ -110,14 +110,13 @@ case $arch_spec in ARCH=`/usr/bin/arch` elif test -f /usr/ucb/arch ; then ARCH=`/usr/ucb/arch` - elif test -f /bin/uname ; then - ARCH=`/bin/uname -m` + elif /bin/uname -s | grep -q -i CYGWIN ; then + ARCH=win32 else echo "I can not automatically find the name of your architecture" echo -n\ "Give me a name, please [win32 for Win95, Win98 or WinNT]: " read ARCH - fi;; yes) ARCH=$arch esac @@ -444,7 +443,8 @@ let camlp4lib = "$CAMLP4LIB" let best = "$best_compiler" let arch = "$ARCH" let osdeplibs = "$OSDEPLIBS" -(* let defined = [ "$OSTYPE" ] *) +(* this does seem to be used any longer +let defined = [ "$OSTYPE" ] *) let version = "$VERSION" let versionsi = "$VERSIONSI" let date = "$DATE" |