patch to "display"
authorpaulson
Fri Oct 01 11:54:15 2004 +0200 (2004-10-01)
changeset 15223e669fb5b0f5a
parent 15222 2406fd8a5c30
child 15224 1bd35fd87963
patch to "display"
lib/Tools/display
     1.1 --- a/lib/Tools/display	Fri Oct 01 11:53:50 2004 +0200
     1.2 +++ b/lib/Tools/display	Fri Oct 01 11:54:15 2004 +0200
     1.3 @@ -76,8 +76,8 @@
     1.4  [ -f "$FILE" ] || fail "Bad file: $FILE"
     1.5  
     1.6  if [ -n "$CLEAN" ]; then
     1.7 -  PRIVATE_FILE="$ISABELLE_TMP_PREFIX/"$$"$FILE"
     1.8 -  mv "$FILE" "$PRIVATE_FILE" || fail "Cannot move file: $FILE"
     1.9 +  PRIVATE_FILE="$ISABELLE_TMP/"$(basename "$FILE")
    1.10 +  mv "$FILE" "$PRIVATE_FILE" ##|| fail "Cannot move file: $FILE"
    1.11    view "$PRIVATE_FILE"
    1.12    rm -f "$PRIVATE_FILE"
    1.13  else