--- 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) =>