diff options
| -rw-r--r-- | distrib/Makefile | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/distrib/Makefile b/distrib/Makefile index cc46418c66..88f870a478 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} |