-
Notifications
You must be signed in to change notification settings - Fork 1.5k
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
Add Default to Clippy Lints Lint groups #9616
Conversation
r? @dswij (rust-highfive has picked a reviewer for you, use r? to override) |
r? @xFrednet I think you are the best reviewer for this. Should the The |
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.
Overall looks good to me, two smaller suggestions
util/gh-pages/script.js
Outdated
$scope.resetGroupsToDefault = function () { | ||
const groups = $scope.groups; | ||
for (const [key, value] of Object.entries(GROUPS_FILTER_DEFAULT)) { | ||
if (groups.hasOwnProperty(key)) { |
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.
This should always be true, shouldn't it?
I think default should reset to the default of the lint list. If we only want it to be warn-by-default lints, then that should also be the default of the list IMO. With context, I think that this is already covered by the lint level selection. We could maybe add a second button, which is |
@xFrednet Thanks, I added a commit for your suggestion. |
Makes sense to me. I don't think there is a need for a button for |
Looks good to me and runs perfectly. Thank you for the changes! @bors r+ |
☀️ Test successful - checks-action_dev_test, checks-action_remark_test, checks-action_test |
This PR adds a default (reset) button to Clippy Lints Lint groups. (change for website)
The page sets only
Deprecated
to false by default.Certainly it is easy to set only
deprecated
to false, but it may be a bit lazy for beginners.Screen.Recording.2022-10-10.at.17.58.52.mov
changelog: none