diff options
| author |  Stephane Glondu <steph@glondu.net> | 2012-08-20 18:27:01 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2012-08-20 18:27:01 +0200 |
| commit | e0d682ec25282a348d35c5b169abafec48555690 (patch) | |
| tree | 1a46f0142a85df553388c932110793881f3af52f /.gitignore | |
| parent | 86535d84cc3cffeee1dcd8545343f234e7285530 (diff) | |
Imported Upstream version 8.4dfsgupstream/8.4dfsg
Diffstat (limited to '.gitignore')
| -rw-r--r-- | .gitignore | 5 |
1 files changed, 3 insertions, 2 deletions
@@ -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 |