# HG changeset patch # User wenzelm # Date 1489417573 -3600 # Node ID 73ba79126b55602fa7d229a1c58e7c7c7411e06a # Parent 8cfdf420b64317e243bf0cf7c176e551e3d92fb8 tuned; diff -r 8cfdf420b643 -r 73ba79126b55 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Mon Mar 13 15:59:00 2017 +0100 +++ b/src/Pure/Tools/build.scala Mon Mar 13 16:06:13 2017 +0100 @@ -199,23 +199,10 @@ } })) - def session_dependencies( - options: Options, - inlined_files: Boolean, - dirs: List[Path], - sessions: List[String]): Deps = + def session_base(options: Options, session: String, dirs: List[Path] = Nil): Sessions.Base = { - val (_, tree) = Sessions.load(options, dirs = dirs).selection(sessions = sessions) - dependencies(inlined_files = inlined_files, tree = tree) - } - - def session_base( - options: Options, - session_name: String, - session_dirs: List[Path] = Nil, - inlined_files: Boolean = false): Sessions.Base = - { - session_dependencies(options, inlined_files, session_dirs, List(session_name))(session_name) + val (_, tree) = Sessions.load(options, dirs = dirs).selection(sessions = List(session)) + dependencies(tree = tree)(session) }