lib/scripts/getsettings
changeset 61319 d84b4d39bce1
parent 61294 2d3d26e9b191
child 62354 fdd6989cc8a0
     1.1 --- a/lib/scripts/getsettings	Fri Oct 02 20:28:56 2015 +0200
     1.2 +++ b/lib/scripts/getsettings	Fri Oct 02 23:22:49 2015 +0200
     1.3 @@ -271,8 +271,12 @@
     1.4  #main components
     1.5  init_component "$ISABELLE_HOME"
     1.6  [ -d "$ISABELLE_HOME/Admin" ] && init_component "$ISABELLE_HOME/Admin"
     1.7 -[ -d "$ISABELLE_HOME_USER" ] && init_component "$ISABELLE_HOME_USER"
     1.8 -
     1.9 +if [ -d "$ISABELLE_HOME_USER" ]; then
    1.10 +  init_component "$ISABELLE_HOME_USER"
    1.11 +else
    1.12 +  mkdir -p "$ISABELLE_HOME_USER"
    1.13 +  chmod $(umask -S) "$ISABELLE_HOME_USER"
    1.14 +fi
    1.15  
    1.16  #ML system identifier
    1.17  if [ -z "$ML_PLATFORM" ]; then