diff options
author | 2003-12-28 22:05:25 +0000 | |
---|---|---|
committer | 2003-12-28 22:05:25 +0000 | |
commit | 5522a818a864e789dc0f05fc0ceca52cf29f3dd8 (patch) | |
tree | d91acdcb8c27e4c4b3555b3a9b7d697b5aff5bfd /distrib/configure.distrib | |
parent | e5ee96a918963f9e92bde8b9555b5f6132e9e298 (diff) |
MAJ 8.0
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5158 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'distrib/configure.distrib')
-rwxr-xr-x | distrib/configure.distrib | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/distrib/configure.distrib b/distrib/configure.distrib index b017b8c83..ac52c65b2 100755 --- a/distrib/configure.distrib +++ b/distrib/configure.distrib @@ -31,7 +31,8 @@ case $ANSWER in esac DASHEDVERSION=V`echo $VERSION | sed -e 's/\./-/g'` -MAJORVERSION=V`echo $VERSION | sed -e 's/^\([0-9]\)\.[0-9].*/\1/'` +#MAJORVERSION=V`echo $VERSION | sed -e 's/^\([0-9]\)\.[0-9].*/\1/'` +MAJORVERSION=V7 MAINNUMBER=`echo $VERSION | sed -e 's/\(.*\)\.[0-9]*$/\1/'` LASTNUMBER=`echo $VERSION | sed -e 's/.*\.\([0-9]*\)$/\1/'` if [ "$LASTNUMBER" = "0" ]; then |