diff options
| author | herbelin | 2001-09-25 07:37:52 +0000 |
|---|---|---|
| committer | herbelin | 2001-09-25 07:37:52 +0000 |
| commit | 7b56283ddc0c2b3be8ab4a76a451eac6319d4235 (patch) | |
| tree | d0d7c98401c263aa29933139453f093fc96f7a7f | |
| parent | f5c0396f5ff4a1357f954fccd725ca68e40bd62c (diff) | |
MAJ V7.1
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2064 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | distrib/Makefile | 14 | ||||
| -rw-r--r-- | distrib/RELEASE | 9 | ||||
| -rwxr-xr-x | distrib/configure.distrib | 2 |
3 files changed, 11 insertions, 14 deletions
diff --git a/distrib/Makefile b/distrib/Makefile index 9ea3ca6ce8..77ac42e383 100644 --- a/distrib/Makefile +++ b/distrib/Makefile @@ -50,10 +50,8 @@ rpm: src-rpm arch-rpm ################# tag: - @dashedversion=V`echo ${VERSION} | sed -e 's/\./-/g'`;\ - majorversion=V`echo ${VERSION} | sed -e 's/^\([0-9]\.[0-9]\).*/\1/g'`;\ - echo -n "Tagging the archive with version number $$dashedversion... ";\ - cvs rtag -F $$dashedversion $$majorversion + echo -n "Tagging the archive with version number $(DASHEDVERSION)...";\ + cvs rtag -F $(DASHEDVERSION) $(MAJORVERSION) tar-gz: @echo -n Exporting a fresh copy of the archive... @@ -198,16 +196,14 @@ coq.spec: RH/coq.list RH/coq.spec.tpl ########## contrib-tag: - @dashedversion=V`echo ${VERSION} | sed -e 's/\./-/g'`;\ - echo -n "Tagging the contrib with version number $$dashedversion... ";\ - cvs rtag -F $$dashedversion contrib + echo -n "Tagging the contrib with version number $(DASHEDVERSION)...";\ + cvs rtag -F $(DASHEDVERSION) contrib @echo done contrib-tar-gz: - rm -rf contrib-${VERSION} @echo -n Exporting a fresh copy of the contribs... - @dashedversion=V`echo ${VERSION} | sed -e 's/\./-/g'`;\ - cvs export -d contrib-${VERSION} -r $$dashedversion contrib + cvs export -d contrib-${VERSION} -r $(DASHEDVERSION) contrib @echo done - rm contrib-${VERSION}.tar.gz @echo -n Building the tar.gz contrib package diff --git a/distrib/RELEASE b/distrib/RELEASE index 1776d4dc4c..e8702134e1 100644 --- a/distrib/RELEASE +++ b/distrib/RELEASE @@ -74,10 +74,11 @@ frais (obtenu par cvs export) de l'archive avec make tar-gz - En particulier, les fichiers à ne pas distribuer (dont la doc) sont -retirés. Cette commande fait dérouler une check-list. Si on -l'interrompt ou qu'elle échoue, le tar-gz reste créé et c'est à la -charge de l'utilisateur de s'assurer que les paramètres sont corrects. + En particulier, les fichiers à ne pas distribuer (dont le répertoire +distrib, le TODO, etc) sont retirés. Cette commande fait dérouler une +check-list. Si on l'interrompt ou qu'elle échoue, le tar-gz reste créé +et c'est à la charge de l'utilisateur de s'assurer que les paramètres +sont corrects. Pour l'installation sous ftp voir A7. diff --git a/distrib/configure.distrib b/distrib/configure.distrib index 5bb5e7657c..c27518ef55 100755 --- a/distrib/configure.distrib +++ b/distrib/configure.distrib @@ -27,7 +27,7 @@ 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/'` MAINNUMBER=`echo $VERSION | sed -e 's/\(.*\)\.[0-9]*$/\1/'` LASTNUMBER=`echo $VERSION | sed -e 's/.*\.\([0-9]*\)$/\1/'` if [ "$LASTNUMBER" = "0" ]; then |