diff -r 79b120d1c1a3 -r ec52a1a6ed31 src/Pure/library.scala
--- a/src/Pure/library.scala	Wed Mar 03 21:37:20 2021 +0100
+++ b/src/Pure/library.scala	Wed Mar 03 21:58:29 2021 +0100
@@ -148,7 +148,7 @@
   def isolate_substring(s: String): String = new String(s.toCharArray)
 
   def strip_ansi_color(s: String): String =
-    s.replaceAll("""\u001b\[\d+m""", "")
+    s.replaceAll("\u001b\\[\\d+m", "")
 
 
   /* quote */