aboutsummaryrefslogtreecommitdiffhomepage
path: root/.gitignore
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-05-30 17:08:09 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-05-30 17:08:09 +0000
commit1a09d9d0635ebd5f5be5f4165438db9122278fd2 (patch)
treebe0b1906ce5d387e338c53abcc9f397b33b364e5 /.gitignore
parent4d58a4f25a796d1c5d39f2be8648696cdfd46dba (diff)
Adds Reference-Manual.out to .gitignore
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15401 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to '.gitignore')
-rw-r--r--.gitignore5
1 files changed, 3 insertions, 2 deletions
diff --git a/.gitignore b/.gitignore
index 0cbb48297..1f41ade07 100644
--- a/.gitignore
+++ b/.gitignore
@@ -63,11 +63,12 @@ doc/refman/csdp.cache
doc/refman/trace
doc/refman/Reference-Manual.pdf
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/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