update gitignore
authorChristian Grothoff <christian@grothoff.org>
Fri, 29 Jun 2018 14:10:25 +0000 (16:10 +0200)
committerChristian Grothoff <christian@grothoff.org>
Fri, 29 Jun 2018 14:10:25 +0000 (16:10 +0200)
commita5a879c7462f9f1628d2372907a645d9dcaaccf1
tree8d7a3adf10fd3ca799799d3446930f58862a1627
parentb7a1d538eb03e2ac87149f2823c1e616b13bad93
update gitignore
src/util/.gitignore