src/Pure/Tools/build.scala
changeset 65210 8cfdf420b643
parent 64909 8007f10195af
child 65211 73ba79126b55
     1.1 --- a/src/Pure/Tools/build.scala	Mon Mar 13 15:32:19 2017 +0100
     1.2 +++ b/src/Pure/Tools/build.scala	Mon Mar 13 15:59:00 2017 +0100
     1.3 @@ -211,16 +211,13 @@
     1.4  
     1.5    def session_base(
     1.6      options: Options,
     1.7 -    inlined_files: Boolean,
     1.8 -    dirs: List[Path],
     1.9 -    session: String): Sessions.Base =
    1.10 +    session_name: String,
    1.11 +    session_dirs: List[Path] = Nil,
    1.12 +    inlined_files: Boolean = false): Sessions.Base =
    1.13    {
    1.14 -    session_dependencies(options, inlined_files, dirs, List(session))(session)
    1.15 +    session_dependencies(options, inlined_files, session_dirs, List(session_name))(session_name)
    1.16    }
    1.17  
    1.18 -  def outer_syntax(options: Options, dirs: List[Path], session: String): Outer_Syntax =
    1.19 -    session_base(options, false, dirs, session).syntax
    1.20 -
    1.21  
    1.22    /* jobs */
    1.23