proper shell variable;
authorwenzelm
Fri Jul 27 16:27:26 2012 +0200 (2012-07-27 ago)
changeset 48553a4893c509aa2
parent 48552 b1819875b76a
child 48554 011cbb395d46
proper shell variable;
etc/settings
     1.1 --- a/etc/settings	Fri Jul 27 15:37:48 2012 +0200
     1.2 +++ b/etc/settings	Fri Jul 27 16:27:26 2012 +0200
     1.3 @@ -97,7 +97,7 @@
     1.4  ###
     1.5  
     1.6  # The place for user configuration, heap files, etc.
     1.7 -if [ -z "ISABELLE_IDENTIFIER" ]; then
     1.8 +if [ -z "$ISABELLE_IDENTIFIER" ]; then
     1.9    ISABELLE_HOME_USER="$USER_HOME/.isabelle"
    1.10  else
    1.11    ISABELLE_HOME_USER="$USER_HOME/.isabelle/$ISABELLE_IDENTIFIER"