author | wenzelm |
Sat, 18 Mar 2017 14:16:13 +0100 | |
changeset 65305 | bec8674aa6ec |
parent 65304 | fd6415b8c0a9 |
child 65306 | eab556c6037d |
--- a/src/Pure/PIDE/batch_session.scala Sat Mar 18 14:12:38 2017 +0100 +++ b/src/Pure/PIDE/batch_session.scala Sat Mar 18 14:16:13 2017 +0100 @@ -26,7 +26,7 @@ if (!Build.build(options, new Console_Progress(verbose = verbose), verbose = verbose, build_heap = true, dirs = dirs, sessions = List(parent_session)).ok) - new RuntimeException + throw new RuntimeException val deps = Sessions.dependencies(verbose = verbose, tree = session_tree) val resources = new Resources(deps(parent_session))