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
 }