aboutsummaryrefslogtreecommitdiffhomepage
path: root/distrib/configure.distrib
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-12-28 22:05:25 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-12-28 22:05:25 +0000
commit5522a818a864e789dc0f05fc0ceca52cf29f3dd8 (patch)
treed91acdcb8c27e4c4b3555b3a9b7d697b5aff5bfd /distrib/configure.distrib
parente5ee96a918963f9e92bde8b9555b5f6132e9e298 (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-xdistrib/configure.distrib3
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