diff --git a/configure b/configure index b920ddea1c..faaee7f715 100755 --- a/configure +++ b/configure @@ -417,7 +417,7 @@ EOF else cat <