more explicit umask for important directories: e.g. relevant for Windows 10, where implicit g=rwx leads to odd failure of chmod -w for heap images;

--- a/bin/isabelle_process	Fri Oct 02 20:28:56 2015 +0200
+++ b/bin/isabelle_process	Fri Oct 02 23:22:49 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!

--- a/lib/scripts/getsettings	Fri Oct 02 20:28:56 2015 +0200
+++ b/lib/scripts/getsettings	Fri Oct 02 23:22:49 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