From 72c35b310a7b8a23934a1e9632d4d989c184d0d7 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 16 Apr 2018 18:16:37 +0200
Subject: Remove LaTeX refman, now that migration to Sphinx is complete

---
 Makefile | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index c31534f36c..793afb661e 100644
--- a/Makefile
+++ b/Makefile
@@ -235,11 +235,8 @@ docclean:
 	  doc/stdlib/*Library.coqdoc.tex doc/stdlib/library.files \
 	  doc/stdlib/library.files.ls doc/stdlib/FullLibrary.tex
 	rm -f doc/*/*.ps doc/*/*.pdf doc/*/*.eps doc/*/*.pdf_t doc/*/*.eps_t
-	rm -rf doc/refman/html doc/stdlib/html doc/tutorial/tutorial.v.html
-	rm -f doc/refman/euclid.ml doc/refman/euclid.mli
-	rm -f doc/refman/heapsort.ml doc/refman/heapsort.mli
+	rm -rf doc/stdlib/html doc/tutorial/tutorial.v.html
 	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 -rf doc/sphinx/_build
 
-- 
cgit v1.2.3