# HG changeset patch
# User wenzelm
# Date 1489842973 -3600
# Node ID bec8674aa6ec9557fdf5e076a1790fd4e19dc582
# Parent  fd6415b8c0a917e9e549c02973f95632d3367344
actually throw exception;

diff -r fd6415b8c0a9 -r bec8674aa6ec src/Pure/PIDE/batch_session.scala
--- 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))