# HG changeset patch
# User wenzelm
# Date 1343399246 -7200
# Node ID a4893c509aa289c67f9b3684ca80f03613d62919
# Parent  b1819875b76abec577dbcaf855dc65df4b3a6574
proper shell variable;

diff -r b1819875b76a -r a4893c509aa2 etc/settings
--- 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"