diff -r 26fc70e983c2 -r ba9dcdbf45f1 lib/Tools/browser
--- a/lib/Tools/browser	Tue Sep 25 15:40:41 2012 +0200
+++ b/lib/Tools/browser	Tue Sep 25 16:48:33 2012 +0200
@@ -72,9 +72,9 @@
 if [ -n "$GRAPHFILE" ]; then
   PRIVATE_FILE="${ISABELLE_TMP:-/tmp}/$$"$(basename "$GRAPHFILE")
   if [ -n "$CLEAN" ]; then
-    mv -f "$GRAPHFILE" "$PRIVATE_FILE" || fail "Cannot move file: $FILE"
+    mv -f "$GRAPHFILE" "$PRIVATE_FILE" || fail "Cannot move file: $GRAPHFILE"
   else
-    cp -f "$GRAPHFILE" "$PRIVATE_FILE" || fail "Cannot copy file: $FILE"
+    cp -f "$GRAPHFILE" "$PRIVATE_FILE" || fail "Cannot copy file: $GRAPHFILE"
   fi
 
   PDF=""