# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1719837090 -7200
# Node ID 010d45681b8788f2786ea6006051e7c0a9a00e39
# Parent  8506bfd25efb4629355d87bfa5e9ac68680baadf
tuned website;

diff -r 8506bfd25efb -r 010d45681b87 src/Pure/Build/build_manager.scala
--- 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)
               }
             }