aboutsummaryrefslogtreecommitdiffhomepage
path: root/distrib/RELEASE
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-09-25 07:37:52 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-09-25 07:37:52 +0000
commit7b56283ddc0c2b3be8ab4a76a451eac6319d4235 (patch)
treed0d7c98401c263aa29933139453f093fc96f7a7f /distrib/RELEASE
parentf5c0396f5ff4a1357f954fccd725ca68e40bd62c (diff)
MAJ V7.1
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2064 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'distrib/RELEASE')
-rw-r--r--distrib/RELEASE9
1 files changed, 5 insertions, 4 deletions
diff --git a/distrib/RELEASE b/distrib/RELEASE
index 1776d4dc4..e8702134e 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.