From cb16f994e14073ab5731beeffc05ea114001d8e1 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 2 Oct 2018 21:38:55 +0200
Subject: [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.
---
 Makefile | 12 +++---------
 1 file changed, 3 insertions(+), 9 deletions(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 2e4f46272e..a15870faca 100644
--- a/Makefile
+++ b/Makefile
@@ -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.
-- 
cgit v1.2.3