fix #5431
authorChristian Grothoff <christian@grothoff.org>
Tue, 20 Nov 2018 23:08:00 +0000 (00:08 +0100)
committerChristian Grothoff <christian@grothoff.org>
Tue, 20 Nov 2018 23:08:31 +0000 (00:08 +0100)
commit1816097b7a4dca73a163b89c243ebf855e371ae5
tree3fe4f766a146dd3bb4af96e04a6871e6cfd2020b
parent14180e7ab413f6759b484a9565bc91b895d4c132
fix #5431
configure.ac