# HG changeset patch # User wenzelm # Date 1398250315 -7200 # Node ID 56335a8e2e8bdf53b24d74f4fb45ad88f6fcb2c3 # Parent 65e84b0ef974d637982f6f33614633b4a8ec4dba interruptible dependencies, which can take a few seconds; diff -r 65e84b0ef974 -r 56335a8e2e8b src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Wed Apr 23 12:39:23 2014 +0200 +++ b/src/Pure/Tools/build.scala Wed Apr 23 12:51:55 2014 +0200 @@ -423,6 +423,8 @@ verbose: Boolean, list_files: Boolean, tree: Session_Tree): Deps = Deps((Map.empty[String, Session_Content] /: tree.topological_order)( { case (deps, (name, info)) => + if (progress.stopped) throw Exn.Interrupt() + try { val (preloaded, parent_syntax) = info.parent match {