update ignore
authorChristian Grothoff <christian@grothoff.org>
Sun, 20 May 2018 21:56:07 +0000 (23:56 +0200)
committerChristian Grothoff <christian@grothoff.org>
Sun, 20 May 2018 21:56:07 +0000 (23:56 +0200)
commit1477e20bacf5d3d29adb5622c8317dfd0f8731b4
treee465fb703588786310fea767328caf4eb7ff52e5
parent6fd410f8e3f1386cc825889a4c9054d3215f03f5
update ignore
doc/documentation/.gitignore