src/Pure/Thy/sessions.scala
changeset 66573 a6401a6417cf
parent 66571 0fdeb24e535e
child 66575 191048506504
     1.1 --- a/src/Pure/Thy/sessions.scala	Thu Aug 31 16:35:09 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Thu Aug 31 17:21:38 2017 +0200
     1.3 @@ -307,10 +307,8 @@
     1.4      dirs: List[Path] = Nil,
     1.5      all_known: Boolean = false): Base =
     1.6    {
     1.7 -    session_base_errors(options, session, dirs = dirs, all_known = all_known) match {
     1.8 -      case (Nil, base) => base
     1.9 -      case (errs, _) => error(cat_lines(errs))
    1.10 -    }
    1.11 +    val (errs, base) = session_base_errors(options, session, dirs = dirs, all_known = all_known)
    1.12 +    if (errs.isEmpty) base else error(cat_lines(errs))
    1.13    }
    1.14  
    1.15