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

Show lint names #6325

Closed
wants to merge 2 commits into from
Closed

Show lint names #6325

wants to merge 2 commits into from

Conversation

sammykim
Copy link
Contributor

@sammykim sammykim commented May 8, 2013

Fix #3525.

@sammykim
Copy link
Contributor Author

sammykim commented May 9, 2013

Done.

bors added a commit that referenced this pull request May 9, 2013
@bors
auto merge of #6325 : sammykim/rust/lint-name, r=graydon
7a4c6e5 
Fix #3525.
@bors bors closed this May 9, 2013
@alexcrichton
Copy link
Member

When merging this with #6093, I went ahead and made these a bit more specific. It's not always the case that -W should be in front from what I could tell. There's three different cases of source emission now:

  • The lint level was by default, and the message has [(warn|forbid|deny) by default]
  • The lint level was set by the command line, and the appended message is [-(W|D|F) lint-name]
  • The lint level was set by some attribute, in which case a span_note is emitted with the source of the lint source.

Does that sound ok to you?

@sanxiyn
Copy link
Member

sanxiyn commented May 9, 2013

@alexcrichton The idea of #3525 was that the lint should always show its name so that its setting can be changed. [warn by default] would not accomplish that.

@alexcrichton
Copy link
Member

hmm... good point, I think I'll change it to [-W unused-imports (default)] just so it's known that it's a default instead of being passed on the command line.

flip1995 pushed a commit to flip1995/rust that referenced this pull request Nov 20, 2020
@bors
Auto merge of rust-lang#6325 - flip1995:rustup, r=flip1995
bd13a35 
Rustup

r? `@ghost`

changelog: none
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
6 participants
@sammykim @alexcrichton @sanxiyn @graydon @z0w0 @bors