summaryrefslogtreecommitdiff
path: root/manual/.gitignore
diff options
context:
space:
mode:
Diffstat (limited to 'manual/.gitignore')
-rw-r--r--manual/.gitignore2
1 files changed, 2 insertions, 0 deletions
diff --git a/manual/.gitignore b/manual/.gitignore
index 7412c4d4..8ae9cbde 100644
--- a/manual/.gitignore
+++ b/manual/.gitignore
@@ -6,4 +6,6 @@
*.out
*.pdf
*.toc
+*.snm
+*.nav
*.ok