diff options
| -rw-r--r-- | .gitignore | 16 |
1 files changed, 15 insertions, 1 deletions
diff --git a/.gitignore b/.gitignore index 292e9d8a7c..948cd98d7b 100644 --- a/.gitignore +++ b/.gitignore @@ -50,12 +50,26 @@ doc/refman/Reference-Manual.pdf doc/refman/Reference-Manual.ps doc/refman/cover.html doc/refman/styles.hva +doc/refman/Reference-Manual.html +doc/common/version.tex +doc/refman/Reference-Manual.sh +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.pdf doc/stdlib/Library.ps +doc/stdlib/Library.coqdoc.tex +doc/stdlib/html/ +doc/stdlib/index-body.html +doc/stdlib/index-list.html doc/RecTutorial/RecTutorial.html doc/RecTutorial/RecTutorial.pdf doc/RecTutorial/RecTutorial.ps _build plugins/*/*_mod.ml -myocamlbuild_config.ml
\ No newline at end of file +myocamlbuild_config.ml |