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