# HG changeset patch
# User wenzelm
# Date 1259511819 -3600
# Node ID d4d430dfabc6f497fed38914fd625e1d99d0fd0c
# Parent  3711139cffc34d3d8a948dd2bd8ebd7a965262c6
double check file permissions of write-back image -- more robust for root or administrator on Cygwin;

diff -r 3711139cffc3 -r d4d430dfabc6 bin/isabelle-process
--- a/bin/isabelle-process	Sun Nov 29 17:14:24 2009 +0100
+++ b/bin/isabelle-process	Sun Nov 29 17:23:39 2009 +0100
@@ -181,7 +181,9 @@
 
 case "$OUTPUT" in
   "")
-    [ -z "$READONLY" -a -w "$INFILE" ] && OUTFILE="$INFILE"
+    if [ -z "$READONLY" -a -w "$INFILE" ]; then
+      perl -e "exit (((stat('$INFILE'))[2] & 0222) != 0 ? 0 : 1);" && OUTFILE="$INFILE"
+    fi
     ;;
   */*)
     OUTFILE="$OUTPUT"