diff options
| author | Théo Zimmermann | 2018-10-04 14:06:17 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-10-04 14:06:17 +0200 |
| commit | c1e7333faab2f3b0381fc56aa69979cd80ccd75f (patch) | |
| tree | 55bbf92da12ba1db761fe5f6ef2190a5d430d068 /Makefile | |
| parent | db8b52eb67b4ebeea292a31d5ca16f1332f634f0 (diff) | |
| parent | cb16f994e14073ab5731beeffc05ea114001d8e1 (diff) | |
Merge PR #8636: [doc] [api] Remove `ocamldoc` support in favor of `odoc`
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 12 |
1 files changed, 3 insertions, 9 deletions
@@ -193,11 +193,11 @@ META.coq: META.coq.in # Cleaning ########################################################################### -.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean clean-ide ml4clean depclean cleanconfig distclean voclean timingclean devdocclean alienclean +.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean clean-ide ml4clean depclean cleanconfig distclean voclean timingclean alienclean -clean: objclean cruftclean depclean docclean devdocclean camldevfilesclean +clean: objclean cruftclean depclean docclean camldevfilesclean -cleankeepvo: indepclean clean-ide optclean cruftclean depclean docclean devdocclean +cleankeepvo: indepclean clean-ide optclean cruftclean depclean docclean objclean: archclean indepclean @@ -276,12 +276,6 @@ timingclean: -o -name "time-of-build-before.log" -o -name "time-of-build-after.log" \ -o -name "time-of-build-pretty.log" -o -name "time-of-build-both.log" \) -exec rm -f {} + -devdocclean: - find . \( -name '*.dep.ps' -o -name '*.dot' \) -exec rm -f {} + - rm -f $(OCAMLDOCDIR)/*.log $(OCAMLDOCDIR)/*.aux $(OCAMLDOCDIR)/*.toc - rm -f $(OCAMLDOCDIR)/ocamldoc.sty $(OCAMLDOCDIR)/coq.tex - rm -f $(OCAMLDOCDIR)/html/*.html - # Ensure that every compiled file around has a known source file. # This should help preventing weird compilation failures caused by leftover # compiled files after deleting or moving some source files. |