abort tasks with invalid host specs;
authorFabian Huch <huch@in.tum.de>
Fri, 28 Jun 2024 17:13:25 +0200
changeset 80424 6ed82923d51d
parent 80423 797196669573
child 80449 cba532bf4316
abort tasks with invalid host specs;
src/Pure/Build/build_manager.scala
--- a/src/Pure/Build/build_manager.scala	Fri Jun 28 16:18:40 2024 +0200
+++ b/src/Pure/Build/build_manager.scala	Fri Jun 28 17:13:25 2024 +0200
@@ -739,6 +739,11 @@
 
     private def start_next(): Option[Context] =
       synchronized_database("start_next") {
+        for ((name, task) <- _state.pending if Exn.is_exn(Exn.capture(task.build_hosts))) {
+          progress.echo("Invalid host spec for task " + name + ": " + quote(task.hosts_spec))
+          _state = _state.remove_pending(name)
+        }
+
         _state.next(build_hosts).flatMap { task =>
           echo("Initializing " + task.name)