# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1737117796 -3600
# Node ID f23fc3d21873015db0752d3e105600c0232e7bf8
# Parent  b1f6e80cfff9c60b25347a6134af37c850c1b2a5
tuned whitespace;

diff -r b1f6e80cfff9 -r f23fc3d21873 src/Pure/Build/build_manager.scala
--- a/src/Pure/Build/build_manager.scala	Thu Jan 16 19:00:29 2025 +0100
+++ b/src/Pure/Build/build_manager.scala	Fri Jan 17 13:43:16 2025 +0100
@@ -1411,7 +1411,7 @@
         def render_diff(data: Report.Data, components: List[Component]): XML.Body =
           par(List(page_link(Page.BUILD, "back to build", Markup.Name(build.name)))) ::
           (for (component <- components if !component.is_local) yield {
-            val infos = 
+            val infos =
               data.component_logs.toMap.get(component.name).toList.flatMap(colored) :::
               data.component_diffs.toMap.get(component.name).toList.flatMap(colored)
 
@@ -1508,7 +1508,7 @@
           Web_App.More_HTML.icon("data:image/x-icon;base64," + logo.encode_base64.text),
           HTML.style_file("https://hawkz.github.io/gdcss/gd.css"),
           HTML.style("""
-:root { 
+:root {
   --color-secondary: var(--color-tertiary);
   --color-secondary-hover: var(--color-tertiary-hover);
 }
@@ -1894,7 +1894,7 @@
     progress.interrupt_handler {
       using(store.open_ssh()) { ssh =>
         val user = ssh.execute("whoami").check.out
-        
+
         val build_config = User_Build(user, afp_rev, prefs, requirements, all_sessions,
           base_sessions, exclude_session_groups, exclude_sessions, session_groups, sessions,
           build_heap, clean_build, export_files, fresh_build, presentation, verbose)
diff -r b1f6e80cfff9 -r f23fc3d21873 src/Tools/Find_Facts/src/find_facts.scala
--- a/src/Tools/Find_Facts/src/find_facts.scala	Thu Jan 16 19:00:29 2025 +0100
+++ b/src/Tools/Find_Facts/src/find_facts.scala	Fri Jan 17 13:43:16 2025 +0100
@@ -591,7 +591,7 @@
       Options.Spec.bash_strings(options, bg = true) +
       sessions.map(session => " " + session).mkString
   }
-  
+
   def find_facts_index(
     options: Options,
     sessions: List[String],
@@ -710,13 +710,12 @@
 
       /* index */
 
-      find_facts_index(options, sessions, dirs = dirs, afp_root = afp_root, clean = clean, 
+      find_facts_index(options, sessions, dirs = dirs, afp_root = afp_root, clean = clean,
         progress = progress)
     }
   }
 
 
-
   /** index components **/
 
   def find_facts_index_component(