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 --- .gitignore | 18 ------------------ 1 file changed, 18 deletions(-) (limited to '.gitignore') diff --git a/.gitignore b/.gitignore index 267534365..25c0996cb 100644 --- a/.gitignore +++ b/.gitignore @@ -96,21 +96,6 @@ doc/faq/axioms.eps doc/faq/axioms.eps_t doc/faq/axioms.pdf_t doc/faq/axioms.png -doc/refman/.csdp.cache -doc/refman/trace -doc/refman/Reference-Manual.ps -doc/refman/Reference-Manual.html -doc/refman/Reference-Manual.out -doc/refman/Reference-Manual.sh -doc/refman/cover.html -doc/refman/styles.hva -doc/refman/coqide-queries.eps -doc/refman/coqide.eps -doc/refman/euclid.ml -doc/refman/euclid.mli -doc/refman/heapsort.ml -doc/refman/heapsort.mli -doc/refman/html/ doc/stdlib/Library.out doc/stdlib/Library.ps doc/stdlib/Library.coqdoc.tex @@ -177,9 +162,6 @@ dev/myinclude # coqide generated files (when testing) *.crashcoqide -/doc/refman/Reference-Manual.hoptind -/doc/refman/Reference-Manual.optidx -/doc/refman/Reference-Manual.optind user-contrib .*.sw* -- cgit v1.2.3