| changeset 73355 | ec52a1a6ed31 |
| parent 73344 | f5c147654661 |
| child 73357 | 31d4274f32de |
--- 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 */