# HG changeset patch # User wenzelm # Date 1443820969 -7200 # Node ID d84b4d39bce115f79870692c7351d86003626d8c # Parent a2548e708f03c14df4674c96ab265f579c38f4ff 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; diff -r a2548e708f03 -r d84b4d39bce1 bin/isabelle_process --- 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! diff -r a2548e708f03 -r d84b4d39bce1 lib/scripts/getsettings --- 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