aboutsummaryrefslogtreecommitdiffhomepage
path: root/distrib
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-01-27 17:28:25 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-01-27 17:28:25 +0000
commit9a6180a0fb03bc452414f0327ce375733c223f5d (patch)
tree9872601fe6584611f7618759c08a2782acd0c59c /distrib
parentb84549caa97b373e5ccc5b6ad81592d0c2edb0bf (diff)
Suppression du retrait du répertoire doc de l'archive tar-gzip-ée
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1283 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'distrib')
-rw-r--r--distrib/Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/distrib/Makefile b/distrib/Makefile
index cc46418c6..88f870a47 100644
--- a/distrib/Makefile
+++ b/distrib/Makefile
@@ -60,7 +60,7 @@ tar-gz:
@cvs export -d $(COQPACKAGE) -r $(DASHEDVERSION) $(MAJORVERSION)
@echo done
@echo -n Removing the maintenance files and doc...
- @rm -rf ${COQPACKAGE}/doc
+# @rm -rf ${COQPACKAGE}/doc # doc is implementation doc
@rm -rf ${COQPACKAGE}/distrib
# @rm -rf ${COQPACKAGE}/KNOWN-BUGS
@rm -rf ${COQPACKAGE}/{TODO,ANNONCE,PROBLEMES}