-
-
Notifications
You must be signed in to change notification settings - Fork 3.3k
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.
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
File Browser: add support for filtering directories on search #12342
Conversation
Thanks for making a pull request to jupyterlab! |
3d5ab79
to
84b7278
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Small suggestions otherwise it looks good.
filterDirectories = settings.get('filterDirectories') | ||
.composite as boolean; | ||
|
||
browser.model.filterDirectories = filterDirectories; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It will be nice to refactor all those setters to a single updateFromSettings
function to be connected to settings.changed
and called for initialization.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Sounds good. Either we can do it in this PR. Otherwise happy to track it separately as a 4.0 item but should be done before release, since it is likely to be breaking change.
Co-authored-by: Frédéric Collonval <fcollonval@users.noreply.github.com>
7d085b4
to
effed2d
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks @jtpio
Benchmark reportThe execution time (in milliseconds) are grouped by test file, test type and browser. The mean relative comparison is computed with 95% confidence. Results table
Changes are computed with expected as reference. |
is it too big a change to get it backported to the 3.x release line? I can't wait for this, as my server always launches inside a huge directory with all my repos... thanks for this patch! |
@michaelaye I added it to the list of features for 3.5.0 - feel free to add suggestions of other features you like to see backported. We will look if it is possible (aka not breaking the API). |
@meeseeksdev please backport to 3.5.x |
Owee, I'm MrMeeseeks, Look at me. There seem to be a conflict, please backport manually. Here are approximate instructions:
And apply the correct labels and milestones. Congratulations — you did some good work! Hopefully your backport PR will be tested by the continuous integration and merged soon! Remember to remove the If these instructions are inaccurate, feel free to suggest an improvement. |
… directories on search
…es on search (#13186) Co-authored-by: Jeremy Tuloup <jeremy.tuloup@gmail.com>
References
Fixes #12055
Code changes
Add a setting to also filter directories when searching for files in the file browser.
User-facing changes
In this PR the new setting is true by default.
filter-directories.mp4
Backwards-incompatible changes
None (new parameters are optional).