lib/scripts/getsettings
changeset 33295 ce8faf41b0d4
parent 33294 e2a11715aab1
child 33512 771ec7306438
     1.1 --- a/lib/scripts/getsettings	Wed Oct 28 22:57:32 2009 +0100
     1.2 +++ b/lib/scripts/getsettings	Wed Oct 28 23:21:45 2009 +0100
     1.3 @@ -31,8 +31,6 @@
     1.4  #users tend to put strange things in here ...
     1.5  unset ENV
     1.6  unset BASH_ENV
     1.7 -unset POSIXLY_CORRECT
     1.8 -set +o posix
     1.9  
    1.10  #support easy settings
    1.11  function choosefrom ()
    1.12 @@ -88,7 +86,7 @@
    1.13    local COMPONENT="$1"
    1.14  
    1.15    if [ ! -d "$COMPONENT" ]; then
    1.16 -    echo >&2 "Bad Isabelle component: \"$COMPONENT"\"
    1.17 +    echo >&2 "Bad Isabelle component: \"$COMPONENT\""
    1.18      exit 2
    1.19    elif [ -z "$ISABELLE_COMPONENTS" ]; then
    1.20      ISABELLE_COMPONENTS="$COMPONENT"
    1.21 @@ -107,7 +105,7 @@
    1.22            *) init_component "$COMPONENT/$REPLY" ;;
    1.23          esac
    1.24        done
    1.25 -    } < <( cat "$COMPONENT/etc/components"; echo; )
    1.26 +    } < "$COMPONENT/etc/components"
    1.27    fi
    1.28  }
    1.29