author | paulson |
Fri, 01 Oct 2004 11:54:15 +0200 | |
changeset 15223 | e669fb5b0f5a |
parent 15222 | 2406fd8a5c30 |
child 15224 | 1bd35fd87963 |
lib/Tools/display | file | annotate | diff | comparison | revisions |
--- a/lib/Tools/display Fri Oct 01 11:53:50 2004 +0200 +++ b/lib/Tools/display Fri Oct 01 11:54:15 2004 +0200 @@ -76,8 +76,8 @@ [ -f "$FILE" ] || fail "Bad file: $FILE" if [ -n "$CLEAN" ]; then - PRIVATE_FILE="$ISABELLE_TMP_PREFIX/"$$"$FILE" - mv "$FILE" "$PRIVATE_FILE" || fail "Cannot move file: $FILE" + PRIVATE_FILE="$ISABELLE_TMP/"$(basename "$FILE") + mv "$FILE" "$PRIVATE_FILE" ##|| fail "Cannot move file: $FILE" view "$PRIVATE_FILE" rm -f "$PRIVATE_FILE" else