-
Notifications
You must be signed in to change notification settings - Fork 1.6k
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
Improve display of clippy lints page when JS is disabled #13585
Conversation
2 things I also noticed with the new page:
|
Also the link https://rust-lang.github.io/rust-clippy/master/index.html#cast_possible_truncation doesn't filter the lint list anymore (with or w/o |
Doesn't come from this PR, things are currently broken it seems. Urg. I'll add GUI tests after all fixes have been sent to prevent this situation from happening again. Sending fix for the current page shortly. |
All mentioned bugs were fixed. This PR can be reviewed now. :) |
util/gh-pages/index_template.html
Outdated
<noscript> {# #} | ||
<div class="alert alert-danger" role="alert"> {# #} | ||
Sorry, this site only works with JavaScript! :( {# #} | ||
</div> {# #} | ||
</noscript> {# #} |
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.
Let's leave some kind of message to say the filtering requires JS
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.
Good idea!
Added a CSS class on |
👍 @bors r+ |
☀️ Test successful - checks-action_dev_test, checks-action_remark_test, checks-action_test |
There is no point in displaying the settings menu and the filters if JS is disabled. So in this case, this PR simply hides it:
For the theme handling though, I need to send a fix to mdBook first. But once done, it'll look as expected (dark if system is in dark mode).
changelog: Improve clippy lints page display when JS is disabled.
r? @Alexendoo