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")