equal
deleted
inserted
replaced
60 ## main |
60 ## main |
61 |
61 |
62 [ -f "$FILE" ] || fail "Bad file: $FILE" |
62 [ -f "$FILE" ] || fail "Bad file: $FILE" |
63 |
63 |
64 if [ -n "$CLEAN" ]; then |
64 if [ -n "$CLEAN" ]; then |
65 PRIVATE_FILE=$ISABELLE_TMP/$(basename "$FILE" .dvi)$$.dvi |
65 PRIVATE_FILE="$ISABELLE_TMP/"$(basename "$FILE" .dvi)$$.dvi |
66 mv "$FILE" "$PRIVATE_FILE" || fail "Cannot move file: $FILE" |
66 mv "$FILE" "$PRIVATE_FILE" || fail "Cannot move file: $FILE" |
67 $DVI_VIEWER "$PRIVATE_FILE" |
67 $DVI_VIEWER "$PRIVATE_FILE" |
68 rm -f "$PRIVATE_FILE" |
68 rm -f "$PRIVATE_FILE" |
69 else |
69 else |
70 exec $DVI_VIEWER "$FILE" |
70 exec $DVI_VIEWER "$FILE" |