lib/Tools/display
changeset 44987 fd3a36e48b09
parent 29143 72c960b2b83e
child 47884 21c42b095c84
equal deleted inserted replaced
44986:6f27ecf2a951 44987:fd3a36e48b09
    72 
    72 
    73 if [ -n "$CLEAN" ]; then
    73 if [ -n "$CLEAN" ]; then
    74   PRIVATE_FILE="${ISABELLE_TMP:-/tmp}/$$"$(basename "$FILE")
    74   PRIVATE_FILE="${ISABELLE_TMP:-/tmp}/$$"$(basename "$FILE")
    75   mv "$FILE" "$PRIVATE_FILE" || fail "Cannot move file: $FILE"
    75   mv "$FILE" "$PRIVATE_FILE" || fail "Cannot move file: $FILE"
    76   $VIEWER "$PRIVATE_FILE"
    76   $VIEWER "$PRIVATE_FILE"
    77   sleep 5   #try to avoid races
       
    78   rm -f "$PRIVATE_FILE"
    77   rm -f "$PRIVATE_FILE"
    79 else
    78 else
    80   exec $VIEWER "$FILE"
    79   exec $VIEWER "$FILE"
    81 fi
    80 fi