-
Notifications
You must be signed in to change notification settings - Fork 5.1k
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
Fix top bar visibility not picking up settings overrides (#6833) #6836
Conversation
Here are some expected behaviors in different cases: No default settings override + no user preference override:
Default settings override: visible -> false, adjustToScreen -> false + no user preference override:
(Some other cases, eliminating the outputs and screenshots for easier read.)
|
54b8f9f
to
a314cf7
Compare
a314cf7
to
40e7deb
Compare
Hi @jtpio just a friendly reminder on this PR :) Have you looked at it and/or is there anything I need to add? Thanks! |
@yumyumqing sorry for the late reply! It looks good on Binder and should indeed fix the main usability issue reported in #6833. Looking at the code and the new setting I was wondering if there was a way to combine the two options into a single one. But maybe it's simpler and more explicit to keep the two options separated. |
Hi @jtpio thanks for your response! If we would like to keep the exact same old variables as before to keep users' current overriding files work, I couldn't think of a better way to merge it in 1 variable. Do you have any advice on that? Thanks! |
That sounds like a good idea. JupyterLab uses |
40e7deb
to
6604839
Compare
* Make 'visible' enum type and pick up both default and user settings.
6604839
to
8cdcd9b
Compare
Hi @jtpio I have updated the PR according to our discussion. Could you please help take a look? Thanks a lot! |
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!
visible
box in the settings editor,not
automatically adjust header visibility.Show Header
in menu->view,not
automatically adjust header visibility.uncheck
theadjustToScreen
box in the settings editor,not
automatically adjust header visibility.Show Header
in menu->view,not
automatically adjust header visibility.