diff options
Diffstat (limited to 'manual/.gitignore')
| -rw-r--r-- | manual/.gitignore | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/manual/.gitignore b/manual/.gitignore index 7412c4d4e..8ae9cbdec 100644 --- a/manual/.gitignore +++ b/manual/.gitignore @@ -6,4 +6,6 @@ *.out *.pdf *.toc +*.snm +*.nav *.ok |