From 0b4a387a50e5bc23cf68c854c81ebd7e5c18cc36 Mon Sep 17 00:00:00 2001
From: bayon <wock9000@users.noreply.github.com>
Date: Sat, 11 Jul 2026 22:29:17 -0700
Subject: [PATCH] chore: add .emojiignore to exempt Lean source files from
 emoji gate

Lean uses -> (U+2192) as a built-in type-arrow operator (e.g. Omega -> Real).
This is part of the language syntax, not a decorative status glyph.
---
 .emojiignore | 3 +++
 1 file changed, 3 insertions(+)
 create mode 100644 .emojiignore

diff --git a/.emojiignore b/.emojiignore
new file mode 100644
index 000000000..71182493c
--- /dev/null
+++ b/.emojiignore
@@ -0,0 +1,3 @@
+# Lean source files: -> (U+2192) is the function-type arrow in Lean syntax,
+# not a decorative glyph. All .lean files are excluded from the emoji gate.
+*.lean