diff options
| author | Naveen Nathan <naveen@lastninja.net> | 2019-11-07 11:23:57 +1100 |
|---|---|---|
| committer | Andrew Gallant <jamslam@gmail.com> | 2020-02-17 17:16:28 -0500 |
| commit | 297b428c8c92dca2c62d57dd41ad085aa94c4aa4 (patch) | |
| tree | 37f99ed74be2ffdfeb35e096ac063a0bc813e7e4 /complete | |
| parent | 804b43ecd8bd37fde4fc81f49d1f9bb659aeac1c (diff) | |
cli: add --no-ignore-exclude flag
This commit adds a new --no-ignore-exclude flag that permits disabling
the use of .git/info/exclude filtering. Local exclusions are manual
configurations to a repository and are not shared, so it is sometimes
useful to disable to get a consistent view of a repository.
This also adds a new section to the man page that describes automatic
filtering.
Closes #1420
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 5fa6e9c2..b90d1801 100644 --- a/complete/_rg +++ b/complete/_rg @@ -129,6 +129,10 @@ _rg() { '--ignore-file-case-insensitive[process ignore files case insensitively]' $no'--no-ignore-file-case-insensitive[process ignore files case sensitively]' + + '(ignore-exclude)' # Local exclude (ignore)-file options + "--no-ignore-exclude[don't respect local exclude (ignore) files]" + $no'--ignore-exclude[respect local exclude (ignore) files]' + + '(ignore-global)' # Global ignore-file options "--no-ignore-global[don't respect global ignore files]" $no'--ignore-global[respect global ignore files]' |