ThyInfo.time_use root;
authorwenzelm
Wed, 06 Jul 2005 10:41:49 +0200
changeset 16715 ecca9fd2754f
parent 16714 d9e3ef66b38c
child 16716 57fd954ee326
ThyInfo.time_use root;
src/Pure/Isar/session.ML
--- a/src/Pure/Isar/session.ML	Wed Jul 06 10:41:48 2005 +0200
+++ b/src/Pure/Isar/session.ML	Wed Jul 06 10:41:49 2005 +0200
@@ -79,7 +79,7 @@
       (init reset parent name;
        Present.init build info doc doc_graph (path ()) name
          (if dump = "" then NONE else SOME (Path.unpack dump)) (get_rpath rpath_str) verbose;
-       File.use (Path.basic root);
+       ThyInfo.time_use root;
        finish ())))) ()
   handle exn => (writeln (Toplevel.exn_message exn); exit 1);