# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1743068733 -3600
# Node ID fedac12c7e0e0504c0aa5cfc5f034efb5f7d0f5a
# Parent  882b80bd10c8d992f9adefdb02ccb1fe3c12ae8e
start jobs even if repository is unreachable, e.g. due to high load;

diff -r 882b80bd10c8 -r fedac12c7e0e src/Pure/Build/build_manager.scala
--- a/src/Pure/Build/build_manager.scala	Wed Mar 26 21:11:04 2025 +0000
+++ b/src/Pure/Build/build_manager.scala	Thu Mar 27 10:45:33 2025 +0100
@@ -871,7 +871,10 @@
     val rsync_context = Rsync.Context()
 
     private def sync(repository: Mercurial.Repository, rev: String, target: Path): String = {
-      repository.pull()
+      val pull_result = Exn.capture(repository.pull())
+      if (Exn.is_exn(pull_result)) {
+        echo_error_message("Could not read from repository: " + Exn.the_exn(pull_result).getMessage)
+      }
 
       if (rev.nonEmpty) repository.sync(rsync_context, target, rev = rev)