lib/scripts/getsettings
changeset 45094 a43694a0b726
parent 43519 024bd7f5ee0f
child 46741 a29006291f2b
equal deleted inserted replaced
45093:26f94c72f306 45094:a43694a0b726
    12 ISABELLE_SETTINGS_PRESENT=true
    12 ISABELLE_SETTINGS_PRESENT=true
    13 
    13 
    14 export ISABELLE_HOME
    14 export ISABELLE_HOME
    15 if { echo -n "$ISABELLE_HOME" | fgrep " " >/dev/null; }
    15 if { echo -n "$ISABELLE_HOME" | fgrep " " >/dev/null; }
    16 then
    16 then
    17   echo 1>&2 "### White space in ISABELLE_HOME may cause strange problems later on!"
    17   echo 1>&2 "### White space in ISABELLE_HOME may cause strange problems!"
    18   echo 1>&2 "### ISABELLE_HOME=\"$ISABELLE_HOME\""
    18   echo 1>&2 "### ISABELLE_HOME=\"$ISABELLE_HOME\""
    19 fi
    19 fi
    20 
    20 
    21 #key executables
    21 #key executables
    22 ISABELLE_PROCESS="$ISABELLE_HOME/bin/isabelle-process"
    22 ISABELLE_PROCESS="$ISABELLE_HOME/bin/isabelle-process"