update gitignore
authorChristian Grothoff <christian@grothoff.org>
Tue, 5 Jun 2018 07:45:43 +0000 (09:45 +0200)
committerChristian Grothoff <christian@grothoff.org>
Tue, 5 Jun 2018 07:45:43 +0000 (09:45 +0200)
commit09f7c260e7cd3bc0f12ad89e2dcf7d813f4089d8
treebc4350d1c3852fab1d3653b218ece7a8f62992c6
parent7661f73f0d6def50830323e420ba7b78e791369a
update gitignore
src/util/.gitignore