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