# HG changeset patch
# User berghofe
# Date 870990210 -7200
# Node ID dc998476ce764fcc4fc51a387f3f7347833fecca
# Parent  2b67561c6488a05dcb31fc92c48c65dcc42bb7e4
Modified graph data directory.

diff -r 2b67561c6488 -r dc998476ce76 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;