better fix for #3805
authorChristian Grothoff <christian@grothoff.org>
Mon, 1 Jun 2015 09:28:51 +0000 (09:28 +0000)
committerChristian Grothoff <christian@grothoff.org>
Mon, 1 Jun 2015 09:28:51 +0000 (09:28 +0000)
commitb77b46e3c7b531460391ce8e04098084cb81b829
treef4c1e871291d8bd6d54e575a5cf7df16221a033b
parent16fadb07d078ec5bce5a3d8b498fbc9d0838b9e8
better fix for #3805
configure.ac