summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorChristian Grothoff <christian@grothoff.org>2018-05-20 23:56:07 +0200
committerChristian Grothoff <christian@grothoff.org>2018-05-20 23:56:07 +0200
commit1477e20bacf5d3d29adb5622c8317dfd0f8731b4 (patch)
treee465fb703588786310fea767328caf4eb7ff52e5
parent6fd410f8e3f1386cc825889a4c9054d3215f03f5 (diff)
update ignore
-rw-r--r--doc/documentation/.gitignore7
1 files changed, 7 insertions, 0 deletions
diff --git a/doc/documentation/.gitignore b/doc/documentation/.gitignore
index 2e914d9c9..f490c3412 100644
--- a/doc/documentation/.gitignore
+++ b/doc/documentation/.gitignore
@@ -1,2 +1,9 @@
stamp-1
version2.texi
+manual
+*.fn
+*.fns
+*.ky
+*.pg
+*.tp
+*.vr