Skip to content

Commit 9e4d1bc

Browse files
committed
revert changes to unicode linter
1 parent 9367bb1 commit 9e4d1bc

1 file changed

Lines changed: 0 additions & 6 deletions

File tree

Mathlib/Tactic/Linter/TextBased/UnicodeLinter.lean

Lines changed: 0 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -183,11 +183,6 @@ public def emojis : Array Char := #[
183183
.ofNat 0x1F3C1 -- 🏁️
184184
]
185185

186-
/-- Unicode symbols in mathlib that have no restrictions on which selector they are followed by. -/
187-
public def maybeEmojis : Array Char := #[
188-
'⚠' -- ⚠️
189-
]
190-
191186
/-- Unicode symbols in mathlib that should always be followed by the text variant selector. -/
192187
public def nonEmojis : Array Char := #[]
193188

@@ -215,7 +210,6 @@ public def isAllowedCharacter (c : Char) : Bool :=
215210
|| withVSCodeAbbrev.contains c
216211
|| othersInMathlib.contains c
217212
|| emojis.contains c
218-
|| maybeEmojis.contains c
219213
|| nonEmojis.contains c
220214
|| unrestricted.contains c
221215
|| c == UnicodeVariant.emoji

0 commit comments

Comments
 (0)