aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--mathcomp/Makefile.common2
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/Makefile.common b/mathcomp/Makefile.common
index 04c3adc..857ddef 100644
--- a/mathcomp/Makefile.common
+++ b/mathcomp/Makefile.common
@@ -146,4 +146,4 @@ doc: __always__ Makefile.coq
cp ../etc/artwork/coqdoc.css _build_doc/htmldoc
doc-clean:
- rm -r _build_doc/
+ rm -rf _build_doc/