1
0
mirror of https://github.com/BurntSushi/ripgrep.git synced 2025-01-19 05:49:14 +02:00

ignore/types: add Lean

Ref: https://lean-lang.org/

PR #2678
This commit is contained in:
amesgen 2023-12-07 17:46:00 +01:00 committed by GitHub
parent 5b7a30846f
commit 56c7ad175a
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23

View File

@ -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