double check file permissions of write-back image -- more robust for root or administrator on Cygwin;
authorwenzelm
Sun Nov 29 17:23:39 2009 +0100 (2009-11-29)
changeset 33920d4d430dfabc6
parent 33919 3711139cffc3
child 33921 4c188a74e362
double check file permissions of write-back image -- more robust for root or administrator on Cygwin;
bin/isabelle-process
     1.1 --- a/bin/isabelle-process	Sun Nov 29 17:14:24 2009 +0100
     1.2 +++ b/bin/isabelle-process	Sun Nov 29 17:23:39 2009 +0100
     1.3 @@ -181,7 +181,9 @@
     1.4  
     1.5  case "$OUTPUT" in
     1.6    "")
     1.7 -    [ -z "$READONLY" -a -w "$INFILE" ] && OUTFILE="$INFILE"
     1.8 +    if [ -z "$READONLY" -a -w "$INFILE" ]; then
     1.9 +      perl -e "exit (((stat('$INFILE'))[2] & 0222) != 0 ? 0 : 1);" && OUTFILE="$INFILE"
    1.10 +    fi
    1.11      ;;
    1.12    */*)
    1.13      OUTFILE="$OUTPUT"