# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1720530384 -7200
# Node ID 63afde05a820a6f8aa89402bb619f4035bf8070e
# Parent  417fcf9f5e71f23364971eecfdcc2da16904c409
tuned HTML display of ANSI colors for better readability;

diff -r 417fcf9f5e71 -r 63afde05a820 src/Pure/Build/build_manager.scala
--- a/src/Pure/Build/build_manager.scala	Tue Jul 09 14:13:59 2024 +0200
+++ b/src/Pure/Build/build_manager.scala	Tue Jul 09 15:06:24 2024 +0200
@@ -1261,7 +1261,7 @@
       def render_diff(build: Build, state: State): XML.Body = render_page("Diff: " + build.name) {
         def colored(s: String): XML.Body = {
           val Colored = "([^\u001b]*)\u001b\\[([0-9;]+)m(.*)\u001b\\[0m([^\u001b]*)".r
-          val colors = List("black", "red", "green", "yellow", "blue", "magenta", "cyan", "white")
+          val colors = List("black", "maroon", "green", "olive", "navy", "purple", "teal", "silver")
 
           val lines = split_lines(s).map {
             case Colored(pre, code, s, post) =>