# HG changeset patch
# User wenzelm
# Date 1590224281 -7200
# Node ID 081fdd53003a70d37abf5fdc07e769a1234724c5
# Parent  3882df6a4a931907af957b3892ab855f3b9a82ba
more brackets (see 2e8af171887f);

diff -r 3882df6a4a93 -r 081fdd53003a src/Pure/General/word.scala
--- a/src/Pure/General/word.scala	Sat May 23 10:54:04 2020 +0200
+++ b/src/Pure/General/word.scala	Sat May 23 10:58:01 2020 +0200
@@ -82,6 +82,6 @@
 
   /* brackets */
 
-  val open_brackets = "([{«‹⟨⌈⌊⦇⟦⦃"
-  val close_brackets = ")]}»›⟩⌉⌋⦈⟧⦄"
+  val open_brackets = "([{«‹⟨⌈⌊⦇⟦⦃⟪"
+  val close_brackets = ")]}»›⟩⌉⌋⦈⟧⦄⟫"
 }