equal
deleted
inserted
replaced
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 |