diff options
author | David Torosyan <davidtorosyan.git@gmail.com> | 2019-01-20 17:32:34 -0800 |
---|---|---|
committer | Andrew Gallant <jamslam@gmail.com> | 2019-01-22 20:03:59 -0500 |
commit | 718a00f6f2f88238546f7d33c1ea52217002495e (patch) | |
tree | 6dc4db1c1d1af1f5d87957754341b4f74ff41984 /complete | |
parent | 7cbc535d70a53c81dfa3e58552c01f21c2e38d28 (diff) |
ripgrep: add --ignore-file-case-insensitive
The --ignore-file-case-insensitive flag causes all
.gitignore/.rgignore/.ignore files to have their globs matched without
regard for case. Because this introduces a potentially significant
performance regression, this is always disabled by default. Users that
need case insensitive matching can enable it on a case by case basis.
Closes #1164, Closes #1170
Diffstat (limited to 'complete')
-rw-r--r-- | complete/_rg | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/complete/_rg b/complete/_rg index 6f7b0ef8..f48c0998 100644 --- a/complete/_rg +++ b/complete/_rg @@ -115,6 +115,10 @@ _rg() { "(--no-ignore-global --no-ignore-parent --no-ignore-vcs)--no-ignore[don't respect ignore files]" $no'(--ignore-global --ignore-parent --ignore-vcs)--ignore[respect ignore files]' + + '(ignore-file-case-insensitive)' # Ignore-file case sensitivity options + '--ignore-file-case-insensitive[process ignore files case insensitively]' + $no'--no-ignore-file-case-insensitive[process ignore files case sensitively]' + + '(ignore-global)' # Global ignore-file options "--no-ignore-global[don't respect global ignore files]" $no'--ignore-global[respect global ignore files]' |