author | wenzelm |
Tue, 22 Jun 2004 09:52:15 +0200 | |
changeset 14997 | aa2aaab41566 |
parent 14996 | 2571227f3fcc |
child 14998 | 9606c6224933 |
lib/Tools/display | file | annotate | diff | comparison | revisions |
--- a/lib/Tools/display Tue Jun 22 09:52:08 2004 +0200 +++ b/lib/Tools/display Tue Jun 22 09:52:15 2004 +0200 @@ -62,7 +62,7 @@ [ -f "$FILE" ] || fail "Bad file: $FILE" if [ -n "$CLEAN" ]; then - PRIVATE_FILE=$ISABELLE_TMP/$(basename "$FILE" .dvi)$$.dvi + PRIVATE_FILE="$ISABELLE_TMP/"$(basename "$FILE" .dvi)$$.dvi mv "$FILE" "$PRIVATE_FILE" || fail "Cannot move file: $FILE" $DVI_VIEWER "$PRIVATE_FILE" rm -f "$PRIVATE_FILE"