Ignore index-files

2018-05-22 13:48:30 +02:00 · 2018-05-22 13:48:30 +02:00 · 1683178f1c
parent 01159930de
commit 1683178f1c
1 changed files with 2 additions and 0 deletions
--- a/doc/.gitignore
+++ b/doc/.gitignore
@ -10,3 +10,5 @@
 *.idx
 *.ilg
 *.ind
+*.nav
+*.snm