diff --git a/configure b/configure
index a310d257e449bec8041dc1dd1776241768503805..01b092f37d37834b7ba69c17c1152ac5d81c907c 100755
--- a/configure
+++ b/configure
@@ -313,6 +313,10 @@ sh_quote(){
     echo "$v"
 }
 
+cleanws(){
+    echo "$@" | sed 's/^ *//;s/  */ /g;s/ *$//'
+}
+
 filter(){
     pat=$1
     shift