merged
authorpaulson
Fri, 28 Mar 2025 00:26:18 +0000
changeset 82354 35a219e372b0
parent 82352 fedac12c7e0e (diff)
parent 82353 e3a0128f4905 (current diff)
child 82365 7fee9141da5e
merged
--- a/src/Pure/Build/build_manager.scala	Fri Mar 28 00:26:10 2025 +0000
+++ b/src/Pure/Build/build_manager.scala	Fri Mar 28 00:26:18 2025 +0000
@@ -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)