summaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-06-04 12:07:52 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2012-06-04 12:07:52 +0200
commit61dc740ed1c3780cccaec00d059a28f0d31d0052 (patch)
treed88d05baf35b9b09a034233300f35a694f9fa6c2 /Makefile
parent97fefe1fcca363a1317e066e7f4b99b9c1e9987b (diff)
Imported Upstream version 8.4~gamma0+really8.4beta2upstream/8.4_gamma0+really8.4beta2
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index 876ac583..0ff72856 100644
--- a/Makefile
+++ b/Makefile
@@ -191,6 +191,7 @@ docclean:
rm -f doc/common/version.tex
rm -f doc/refman/styles.hva doc/refman/cover.html doc/refman/Reference-Manual.html
rm -f doc/coq.tex
+ rm -f doc/refman/styles.hva doc/refman/cover.html
archclean: clean-ide optclean voclean
rm -rf _build myocamlbuild_config.ml
@@ -221,7 +222,6 @@ cleanconfig:
rm -f config/Makefile config/coq_config.ml dev/ocamldebug-v7 ide/undo.mli
distclean: clean cleanconfig
- $(MAKE) -C test-suite distclean
voclean:
rm -f states/*.coq