# HG changeset patch
# User wenzelm
# Date 1443890305 -7200
# Node ID 69022bbcd012e3aad784d30d4f1793a55729ec35
# Parent  6a5a188ab3e7222ccd82b355574daea0bed96488# Parent  d84b4d39bce115f79870692c7351d86003626d8c
merged

diff -r 6a5a188ab3e7 -r 69022bbcd012 bin/isabelle_process
--- a/bin/isabelle_process	Sat Oct 03 17:11:04 2015 +0200
+++ b/bin/isabelle_process	Sat Oct 03 18:38:25 2015 +0200
@@ -177,6 +177,7 @@
     ;;
   *)
     mkdir -p "$ISABELLE_OUTPUT"
+    chmod $(umask -S) "$ISABELLE_OUTPUT"
     OUTFILE="$ISABELLE_OUTPUT/$OUTPUT"
     ;;
 esac
@@ -188,6 +189,7 @@
 ISABELLE_PID="$$"
 ISABELLE_TMP="$ISABELLE_TMP_PREFIX$ISABELLE_PID"
 mkdir -p "$ISABELLE_TMP"
+chmod $(umask -S) "$ISABELLE_TMP"
 
 
 ## run it!
diff -r 6a5a188ab3e7 -r 69022bbcd012 lib/scripts/getsettings
--- a/lib/scripts/getsettings	Sat Oct 03 17:11:04 2015 +0200
+++ b/lib/scripts/getsettings	Sat Oct 03 18:38:25 2015 +0200
@@ -271,8 +271,12 @@
 #main components
 init_component "$ISABELLE_HOME"
 [ -d "$ISABELLE_HOME/Admin" ] && init_component "$ISABELLE_HOME/Admin"
-[ -d "$ISABELLE_HOME_USER" ] && init_component "$ISABELLE_HOME_USER"
-
+if [ -d "$ISABELLE_HOME_USER" ]; then
+  init_component "$ISABELLE_HOME_USER"
+else
+  mkdir -p "$ISABELLE_HOME_USER"
+  chmod $(umask -S) "$ISABELLE_HOME_USER"
+fi
 
 #ML system identifier
 if [ -z "$ML_PLATFORM" ]; then