author | wenzelm |
Fri, 27 Jul 2012 16:27:26 +0200 | |
changeset 48553 | a4893c509aa2 |
parent 48552 | b1819875b76a |
child 48554 | 011cbb395d46 |
etc/settings | file | annotate | diff | comparison | revisions |
--- a/etc/settings Fri Jul 27 15:37:48 2012 +0200 +++ b/etc/settings Fri Jul 27 16:27:26 2012 +0200 @@ -97,7 +97,7 @@ ### # The place for user configuration, heap files, etc. -if [ -z "ISABELLE_IDENTIFIER" ]; then +if [ -z "$ISABELLE_IDENTIFIER" ]; then ISABELLE_HOME_USER="$USER_HOME/.isabelle" else ISABELLE_HOME_USER="$USER_HOME/.isabelle/$ISABELLE_IDENTIFIER"