ignore/types: add Lean

Ref: https://lean-lang.org/ PR #2678
BurntSushi · Dec 7, 2023 · 56c7ad1 · 56c7ad1
1 parent 5b7a308
commit 56c7ad1
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/crates/ignore/src/default_types.rs b/crates/ignore/src/default_types.rs
@@ -118,6 +118,7 @@ pub(crate) const DEFAULT_TYPES: &[(&[&str], &[&str])] = &[
     (&["jupyter"], &["*.ipynb", "*.jpynb"]),
     (&["k"], &["*.k"]),
     (&["kotlin"], &["*.kt", "*.kts"]),
+    (&["lean"], &["*.lean"]),
     (&["less"], &["*.less"]),
     (&["license"], &[
         // General