diff options
| author | amesgen <amesgen@amesgen.de> | 2023-12-07 17:46:00 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2023-12-07 11:46:00 -0500 |
| commit | 56c7ad175ac1326e8d36a880061ca3b0e67ad5ea (patch) | |
| tree | 5607c08da6b33a2820c51989894e188fbe4ea7dd | |
| parent | 5b7a30846faba930616b2dce3d2344090330420d (diff) | |
ignore/types: add Lean
Ref: https://lean-lang.org/
PR #2678
| -rw-r--r-- | crates/ignore/src/default_types.rs | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/crates/ignore/src/default_types.rs b/crates/ignore/src/default_types.rs index 04d2d969..329d5418 100644 --- 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 |