diff options
| -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 |