--- a/src/Pure/Build/build_manager.scala Mon Jul 01 13:11:25 2024 +0200
+++ b/src/Pure/Build/build_manager.scala Mon Jul 01 14:31:30 2024 +0200
@@ -1136,8 +1136,8 @@
}
}
- def render_cancelled: XML.Body =
- List(chapter("Build Cancelled"), frontend_link(paths.frontend_url(Page.HOME), text("Home")))
+ def render_cancelled: XML.Body = render_page("Build cancelled")(
+ List(frontend_link(paths.frontend_url(Page.HOME), text("Home"))))
def parse_uuid(params: Params.Data): Option[UUID.T] =
for {
@@ -1182,7 +1182,7 @@
_state = _state
.remove_running(job.name)
.add_running(job1)
- Model.Details(job1, _state, public = false)
+ Model.Cancelled
case result: Result => Model.Details(result, _state, public = false)
}
}