aboutsummaryrefslogtreecommitdiff
path: root/distrib/configure.distrib
diff options
context:
space:
mode:
authorbarras2004-04-07 15:42:30 +0000
committerbarras2004-04-07 15:42:30 +0000
commit33c60bc1be8a4495d2f343d05938521f8194639a (patch)
tree9d922f087d886178dbcd0d7eaf38d619f36ea41f /distrib/configure.distrib
parentbcacb27430bf8b16cf80a460063159e5ae525a57 (diff)
preparation a la release 8.0
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5655 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'distrib/configure.distrib')
-rwxr-xr-xdistrib/configure.distrib1
1 files changed, 0 insertions, 1 deletions
diff --git a/distrib/configure.distrib b/distrib/configure.distrib
index bd4faf442e..bc7ff74e92 100755
--- a/distrib/configure.distrib
+++ b/distrib/configure.distrib
@@ -11,7 +11,6 @@
#
VERSION=`sed -n -e 's/^VERSION=\(.*\)/\1/p' ../configure`
-#VERSIONSI=`sed -n -e 's/^VERSIONSI=\(.*\)/\1/p' ../configure`
DATE=`sed -n -e 's/^DATE=\(.*\)/\1/p' ../configure`
RELEASENUM=1
DISTRIBDIR=`pwd`