diff options
| author | tippfehlr | 2023-04-10 15:09:45 +0000 |
|---|---|---|
| committer | GitHub | 2023-04-10 15:09:45 +0000 |
| commit | 5106a124edc738d5add32a7a862124b9b715e320 (patch) | |
| tree | a55f8c3678db532d15147c533ef27f0c8c71f55d | |
| parent | e72ad1e731877570c6f728e1490485e4b31524a5 (diff) | |
Fix `file-picker.follow-symlinks` config option name in docs (#6685)
| -rw-r--r-- | book/src/configuration.md | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/book/src/configuration.md b/book/src/configuration.md index 4c8ff064..38f9f9eb 100644 --- a/book/src/configuration.md +++ b/book/src/configuration.md @@ -161,7 +161,7 @@ All git related options are only enabled in a git repository. | Key | Description | Default | |--|--|---------| |`hidden` | Enables ignoring hidden files | true -|`follow-links` | Follow symlinks instead of ignoring them | true +|`follow-symlinks` | Follow symlinks instead of ignoring them | true |`deduplicate-links` | Ignore symlinks that point at files already shown in the picker | true |`parents` | Enables reading ignore files from parent directories | true |`ignore` | Enables reading `.ignore` files | true |