Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[file-search] add 'Clear Editor History' command #4392

Merged
merged 1 commit into from
Feb 22, 2019
Merged

[file-search] add 'Clear Editor History' command #4392

merged 1 commit into from
Feb 22, 2019

Commits on Feb 22, 2019

  1. Add 'Clear Editor History' command 

    Fixes #4389

- If a user's recently opened editors list becomes large, there is no way to currently purge the list.
The command helps solve that issue by clearing the location stack, and resetting the pointer.

Signed-off-by: Vincent Fugnitto <[email protected]>
    @vince-fugnitto
    vince-fugnitto committed Feb 22, 2019
    Configuration menu
    Copy the full SHA
    f771509 View commit details
    Browse the repository at this point in the history