lib/Tools/display
changeset 20570 f78dfa306918
parent 15718 f088c10208c0
child 21342 223a3de1222b
equal deleted inserted replaced
20569:c315ba088073 20570:f78dfa306918
    70     *)
    70     *)
    71       fail "Unknown file type: $FILE";
    71       fail "Unknown file type: $FILE";
    72 esac
    72 esac
    73 
    73 
    74 if [ -n "$CLEAN" ]; then
    74 if [ -n "$CLEAN" ]; then
    75   PRIVATE_FILE="$ISABELLE_TMP/$$"$(basename "$FILE")
    75   PRIVATE_FILE="${ISABELLE_TMP:-/tmp}/$$"$(basename "$FILE")
    76   mv "$FILE" "$PRIVATE_FILE" || fail "Cannot move file: $FILE"
    76   mv "$FILE" "$PRIVATE_FILE" || fail "Cannot move file: $FILE"
    77   $VIEWER "$PRIVATE_FILE"
    77   $VIEWER "$PRIVATE_FILE"
       
    78   sleep 5   ;try to avoid races
    78   rm -f "$PRIVATE_FILE"
    79   rm -f "$PRIVATE_FILE"
    79 else
    80 else
    80   exec $VIEWER "$FILE"
    81   exec $VIEWER "$FILE"
    81 fi
    82 fi
    82