src/Pure/Tools/build.ML
changeset 50707 5b2bf7611662
parent 50698 49621c755075
child 50777 20126dd9772c
--- a/src/Pure/Tools/build.ML	Thu Jan 03 15:13:11 2013 +0100
+++ b/src/Pure/Tools/build.ML	Thu Jan 03 20:42:18 2013 +0100
@@ -89,6 +89,10 @@
         | dups => error ("Duplicate document variants: " ^ commas_quote dups));
 
       val _ =
+        (case Session.path () of
+          [] => ()
+        | path => writeln ("\fSession.parent_path = " ^ space_implode "/" path));
+      val _ =
         Session.init do_output false
           (Options.bool options "browser_info") browser_info
           (Options.string options "document")