diff options
| -rw-r--r-- | distrib/Makefile | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/distrib/Makefile b/distrib/Makefile index aecc992347..671987369b 100644 --- a/distrib/Makefile +++ b/distrib/Makefile @@ -251,7 +251,7 @@ patch: ########## clean: - - rm -rf ${COQPACKAGE} ${RPMTOPDIR} ${ARCHBUILDROOT} ${RPMBUILDROOT} + - rm -rf ${COQPACKAGE} ${RPMTOPDIR} ${ARCHBUILDROOT} ${RPMBUILDROOT} RH/build RH/${COQPACKAGE} cleanall: - rm -rf ${COQPACKAGE}* ${RPMTOPDIR} ${ARCHBUILDROOT} ${RPMBUILDROOT} |