aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-04-24 16:17:31 +0000
committerGravatar mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-04-24 16:17:31 +0000
commit06b30bbb3ca957175e1ab884904da13439b9d209 (patch)
treebe507e4802159d741e0b2cf116f8b1e9e3c73134
parent56bc92d843b221afa379dd5cd048ef2676c8af16 (diff)
Retire le repertoire Num
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1691 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--distrib/Makefile3
1 files changed, 2 insertions, 1 deletions
diff --git a/distrib/Makefile b/distrib/Makefile
index 6a3cea54e..255e1572d 100644
--- a/distrib/Makefile
+++ b/distrib/Makefile
@@ -63,8 +63,9 @@ tar-gz:
@echo -n Removing the maintenance files and doc...
# @rm -rf ${COQPACKAGE}/doc # doc is implementation doc
@rm -rf ${COQPACKAGE}/distrib
-# @rm -rf ${COQPACKAGE}/KNOWN-BUGS
+ @rm -rf ${COQPACKAGE}/KNOWN-BUGS
@rm -rf ${COQPACKAGE}/{TODO,ANNONCE,PROBLEMES}
+ @rm -rf ${COQPACKAGE}/theories/Num
@find ${COQPACKAGE} -name ".cvsignore" -exec rm {} \;
@echo done
@echo -n Building the tar.gz source package