update gitignore
authorChristian Grothoff <christian@grothoff.org>
Sun, 1 Jul 2018 17:40:48 +0000 (19:40 +0200)
committerChristian Grothoff <christian@grothoff.org>
Sun, 1 Jul 2018 17:40:48 +0000 (19:40 +0200)
commita62a0839916306a4007d3f2b076878b7a29022ec
tree58037d8ee130ad20f11a3ddff89d38910decd387
parentf726b73c4bdcbfb00b5728dbfaa738f5d6969345
update gitignore
src/util/.gitignore