# 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)
   }