summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2008-08-08 23:14:15 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2008-08-08 23:14:15 +0200
commitff20e3e9f517cba61a94103d62e284b214fe4d30 (patch)
tree5950b1359dab8962bad4f18023f36c8a4c4d85d7
parente6b699f7e1a1ba63c1eb7b7e63094cad633791a9 (diff)
Tune clean target of debian/rules
-rwxr-xr-xdebian/rules5
1 files changed, 5 insertions, 0 deletions
diff --git a/debian/rules b/debian/rules
index 50a6e64f..7a986d94 100755
--- a/debian/rules
+++ b/debian/rules
@@ -59,6 +59,10 @@ clean: unpatch
dh_testroot
rm -f build-stamp configure-stamp opt-stamp install-stamp
+ # Contains a directory ending in .d which breaks the clean rule
+ # of upstream Makefile
+ -rm -Rf debian/coq/etc
+
[ ! -f config/Makefile ] || $(MAKE) clean
[ ! -f config/Makefile ] || $(MAKE) archclean
rm -f bin/*
@@ -67,6 +71,7 @@ clean: unpatch
rm -f dev/ocamldebug-v7
rm -f ide/undo.mli glob.dump
rm -f test-suite/modules/*.vo
+ rm -f doc/stdlib/coqdoc.sty
dh_clean