show expanded path, to avoid odd /foo/bar/$ISABELLE_BROWSER_INFO/baz;
authorwenzelm
Wed Mar 13 14:57:16 2013 +0100 (2013-03-13)
changeset 514158a33d581718b
parent 51410 f0865a641e76
child 51416 e2505a192a7c
show expanded path, to avoid odd /foo/bar/$ISABELLE_BROWSER_INFO/baz;
src/Pure/Thy/present.ML
     1.1 --- a/src/Pure/Thy/present.ML	Wed Mar 13 13:23:16 2013 +0100
     1.2 +++ b/src/Pure/Thy/present.ML	Wed Mar 13 14:57:16 2013 +0100
     1.3 @@ -44,7 +44,7 @@
     1.4  val graph_pdf_path = Path.basic "session_graph.pdf";
     1.5  val graph_eps_path = Path.basic "session_graph.eps";
     1.6  
     1.7 -fun show_path path = Path.implode (Path.append (File.pwd ()) path);
     1.8 +fun show_path path = Path.implode (Path.expand (Path.append (File.pwd ()) path));
     1.9  
    1.10  
    1.11