Skip to content
This repository was archived by the owner on Jul 18, 2026. It is now read-only.

chore: add .emojiignore to exempt Lean source files from emoji gate #2

Merged
wock9000 merged 1 commit into from
Jul 12, 2026
Merged

chore: add .emojiignore to exempt Lean source files from emoji gate #2

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions .emojiignore
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
Loading