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