diff --git a/tools/configure b/tools/configure index 917e963e97..60afbc130a 100755 --- a/tools/configure +++ b/tools/configure @@ -621,6 +621,7 @@ cat <