diff options
| -rw-r--r-- | doc/user/.gitignore | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/doc/user/.gitignore b/doc/user/.gitignore index 3957017..79b70d4 100644 --- a/doc/user/.gitignore +++ b/doc/user/.gitignore @@ -1,4 +1,16 @@ user.html user-*.html +user.tex +user.aux +user.log +user.out +user.dvi +user.toc +user.lout +user.lout.* +user.li* +user.ps +user.pdf *.png +*.jpg *.eps |