mirror of
https://github.com/sharkdp/bat
synced 2026-08-03 18:51:44 +00:00
Merge pull request #2352 from Freed-Wu/extension
Add new file_extensions for INI
This commit is contained in:
+3
@@ -16,6 +16,9 @@ file_extensions:
|
||||
- url
|
||||
- URL
|
||||
- .editorconfig
|
||||
- .coveragerc
|
||||
- .pylintrc
|
||||
- .gitlint
|
||||
- .hgrc
|
||||
- hgrc
|
||||
scope: source.ini
|
||||
|
||||
Reference in New Issue
Block a user