minor fix
authorChristian Grothoff <christian@grothoff.org>
Thu, 16 Aug 2018 12:26:25 +0000 (14:26 +0200)
committerChristian Grothoff <christian@grothoff.org>
Thu, 16 Aug 2018 12:26:25 +0000 (14:26 +0200)
commit8259b96fa0a6797bc853363088bca020cd19b433
tree53012e3f93049042d131d992f1dc885d66a195e6
parentb727497bdeb0487328d470db23ea8cd6e8fdd809
minor fix
configure.ac