# HG changeset patch
# User wenzelm
# Date 1087890735 -7200
# Node ID aa2aaab415660375e324d350e76f2979988dc845
# Parent  2571227f3fcc2e556519aaedb75432e3b004be87
tuned;

diff -r 2571227f3fcc -r aa2aaab41566 lib/Tools/display
--- 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"