# HG changeset patch
# User wenzelm
# Date 1256768505 -3600
# Node ID ce8faf41b0d4600b3472e50cc4faef6a51ee8c0b
# Parent  e2a11715aab1455285f6a79db22ca0810a0eb87a
proper nested quotes;
give up unposixly < <(...) for now -- it needs to be exportable through the global environment (e.g. via make or sh);

diff -r e2a11715aab1 -r ce8faf41b0d4 lib/scripts/getsettings
--- a/lib/scripts/getsettings	Wed Oct 28 22:57:32 2009 +0100
+++ b/lib/scripts/getsettings	Wed Oct 28 23:21:45 2009 +0100
@@ -31,8 +31,6 @@
 #users tend to put strange things in here ...
 unset ENV
 unset BASH_ENV
-unset POSIXLY_CORRECT
-set +o posix
 
 #support easy settings
 function choosefrom ()
@@ -88,7 +86,7 @@
   local COMPONENT="$1"
 
   if [ ! -d "$COMPONENT" ]; then
-    echo >&2 "Bad Isabelle component: \"$COMPONENT"\"
+    echo >&2 "Bad Isabelle component: \"$COMPONENT\""
     exit 2
   elif [ -z "$ISABELLE_COMPONENTS" ]; then
     ISABELLE_COMPONENTS="$COMPONENT"
@@ -107,7 +105,7 @@
           *) init_component "$COMPONENT/$REPLY" ;;
         esac
       done
-    } < <( cat "$COMPONENT/etc/components"; echo; )
+    } < "$COMPONENT/etc/components"
   fi
 }