Modified graph data directory.
authorberghofe
Thu, 07 Aug 1997 23:43:30 +0200
changeset 3639 dc998476ce76
parent 3638 2b67561c6488
child 3640 7554be69fd09
Modified graph data directory.
src/Pure/Thy/browser_info.ML
--- a/src/Pure/Thy/browser_info.ML	Thu Aug 07 23:39:28 1997 +0200
+++ b/src/Pure/Thy/browser_info.ML	Thu Aug 07 23:43:30 1997 +0200
@@ -94,7 +94,7 @@
     in tack_on base rpath end
 in
   val html_path = make_path "html";
-  val graph_path = make_path "graph"
+  val graph_path = make_path "graph/data"
 end;