# HG changeset patch
# User wenzelm
# Date 1504192898 -7200
# Node ID a6401a6417cfd07f23d4249efe20277ab7871c28
# Parent  1e5ae735e026f615f8876aa22a86964e9b736e85
tuned;

diff -r 1e5ae735e026 -r a6401a6417cf src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Thu Aug 31 16:35:09 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Thu Aug 31 17:21:38 2017 +0200
@@ -307,10 +307,8 @@
     dirs: List[Path] = Nil,
     all_known: Boolean = false): Base =
   {
-    session_base_errors(options, session, dirs = dirs, all_known = all_known) match {
-      case (Nil, base) => base
-      case (errs, _) => error(cat_lines(errs))
-    }
+    val (errs, base) = session_base_errors(options, session, dirs = dirs, all_known = all_known)
+    if (errs.isEmpty) base else error(cat_lines(errs))
   }