diff options
| author | Emilio Jesus Gallego Arias | 2018-10-02 21:38:55 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-02 21:38:55 +0200 |
| commit | cb16f994e14073ab5731beeffc05ea114001d8e1 (patch) | |
| tree | e019bbd4ad16afe0f696614562e06d9a5138b52e /Makefile | |
| parent | 24550259892e9e408b11359fa71b240083e7546f (diff) | |
[doc] [api] Remove `ocamldoc` support in favor of `odoc`
This PR removes support for `ocamldoc` in favor of `odoc`.
Following a recent discussion in OCaml's discord, it turns out that
basically all the ecosystem has migrated to odoc, thus we follow suit
and may focus on `odoc` for Coq's ML API documentation.
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. |