show expanded path, to avoid odd /foo/bar/$ISABELLE_BROWSER_INFO/baz;
authorwenzelm
Wed, 13 Mar 2013 14:57:16 +0100
changeset 51415 8a33d581718b
parent 51410 f0865a641e76
child 51416 e2505a192a7c
show expanded path, to avoid odd /foo/bar/$ISABELLE_BROWSER_INFO/baz;
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));