diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-04-16 18:16:37 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-04-16 18:16:37 +0200 |
| commit | 72c35b310a7b8a23934a1e9632d4d989c184d0d7 (patch) | |
| tree | 41182461fb1fc1d626dcb717e675a7ccb9fa656f /.gitignore | |
| parent | 3e7863e9369d38537685576a8642dbe0c062d0c5 (diff) | |
Remove LaTeX refman, now that migration to Sphinx is complete
Diffstat (limited to '.gitignore')
| -rw-r--r-- | .gitignore | 18 |
1 files changed, 0 insertions, 18 deletions
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* |