# HG changeset patch
# User wenzelm
# Date 1363183036 -3600
# Node ID 8a33d581718b0e99049017c274e5576c6090d451
# Parent  f0865a641e762998593761e5749842c7d3d6db2a
show expanded path, to avoid odd /foo/bar/$ISABELLE_BROWSER_INFO/baz;

diff -r f0865a641e76 -r 8a33d581718b src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Wed Mar 13 13:23:16 2013 +0100
+++ b/src/Pure/Thy/present.ML	Wed Mar 13 14:57:16 2013 +0100
@@ -44,7 +44,7 @@
 val graph_pdf_path = Path.basic "session_graph.pdf";
 val graph_eps_path = Path.basic "session_graph.eps";
 
-fun show_path path = Path.implode (Path.append (File.pwd ()) path);
+fun show_path path = Path.implode (Path.expand (Path.append (File.pwd ()) path));