# HG changeset patch # User wenzelm # Date 1505498183 -7200 # Node ID 2e580fcf652236962bc8c8509d85e9d1baa9966e # Parent 1a620647285ceefce7b80472b40078b426843021 avoid local shell variables intruding the resulting environment (via "set -o allexport" in getsettings); diff -r 1a620647285c -r 2e580fcf6522 lib/scripts/getfunctions --- a/lib/scripts/getfunctions Fri Sep 15 17:50:52 2017 +0200 +++ b/lib/scripts/getfunctions Fri Sep 15 19:56:23 2017 +0200 @@ -70,6 +70,7 @@ #classpath function classpath () { + local X="" for X in "$@" do if [ -z "$ISABELLE_CLASSPATH" ]; then @@ -98,6 +99,7 @@ { SPLITARRAY=() local IFS="$1"; shift + local X="" for X in $* do SPLITARRAY["${#SPLITARRAY[@]}"]="$X" @@ -149,6 +151,7 @@ #init component forest function init_components () { + local REPLY="" local BASE="$1" local CATALOG="$2" local COMPONENT=""