lib/Tools/display
changeset 21342 223a3de1222b
parent 20570 f78dfa306918
child 28650 a7ba12e0d3b7
equal deleted inserted replaced
21341:3844037a8e2d 21342:223a3de1222b
    73 
    73 
    74 if [ -n "$CLEAN" ]; then
    74 if [ -n "$CLEAN" ]; then
    75   PRIVATE_FILE="${ISABELLE_TMP:-/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   sleep 5   #try to avoid races
    79   rm -f "$PRIVATE_FILE"
    79   rm -f "$PRIVATE_FILE"
    80 else
    80 else
    81   exec $VIEWER "$FILE"
    81   exec $VIEWER "$FILE"
    82 fi
    82 fi