diff -r d984085c5ff2 -r 7d0c85ad2eec common/autoconf/configure
--- a/common/autoconf/configure	Thu Feb 27 09:40:35 2014 +0100
+++ b/common/autoconf/configure	Fri Feb 28 13:35:32 2014 +0100
@@ -127,10 +127,11 @@
   if [[ -n "$1" ]]; then
     # Uses only shell-safe characters?  No quoting needed.
     # '=' is a zsh meta-character, but only in word-initial position.
-    if [[ "$1" =~ ^[ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789.:,%/+=_-]+$ && ! "$1" =~ ^= ]]; then
+    if echo "$1" | grep -qE '^[ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789.:,%/+=_-]+$' \
+        && ! echo "$1" | grep -qE '^='; then
       quoted="$1"
     else
-      if [[ "$1" =~ [\'!] ]]; then
+      if echo "$1" | grep -qE "[\'!]"; then
         # csh does history expansion within single quotes, but not
         # when backslash-escaped!
         local quoted_quote="'\\''" quoted_exclam="'\\!'"