diff options
| author | Andrew Gallant <jamslam@gmail.com> | 2018-07-22 10:42:32 -0400 |
|---|---|---|
| committer | Andrew Gallant <jamslam@gmail.com> | 2018-07-22 10:42:32 -0400 |
| commit | 560dffd2476f16b4b296aae6aca7aec0f0c6ba1c (patch) | |
| tree | d3dbe91e9179b43b9b0435798b6526c8531152dc /complete | |
| parent | e65ca21a6cebceb9ba79fcd164da24478cc01fb0 (diff) | |
ripgrep: add --no-ignore-global flag
This commit adds a new --no-ignore-global flag that permits disabling
the use of global gitignore filtering. Global gitignores are generally
found in `$HOME/.config/git/ignore`, but its location can be configured
via git's `core.excludesFile` option.
Closes #934
Diffstat (limited to 'complete')
| -rw-r--r-- | complete/_rg | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/complete/_rg b/complete/_rg index b943484d..573467bf 100644 --- a/complete/_rg +++ b/complete/_rg @@ -96,8 +96,12 @@ _rg() { $no"--no-hidden[don't search hidden files and directories]" + '(ignore)' # Ignore-file options - "(--no-ignore-parent --no-ignore-vcs)--no-ignore[don't respect ignore files]" - $no'(--ignore-parent --ignore-vcs)--ignore[respect ignore files]' + "(--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-global)' # Global ignore-file options + "--no-ignore-global[don't respect global ignore files]" + $no'--ignore-global[respect global ignore files]' + '(ignore-parent)' # Parent ignore-file options "--no-ignore-parent[don't respect ignore files in parent directories]" |