diff --git a/configure b/configure index fe7d6b42..5bbff907 100755 --- a/configure +++ b/configure @@ -254,10 +254,13 @@ EOF execute <