diff options
| author | flip1995 <9744647+flip1995@users.noreply.github.com> | 2018-07-30 16:07:00 +0200 |
|---|---|---|
| committer | flip1995 <9744647+flip1995@users.noreply.github.com> | 2018-07-30 16:10:55 +0200 |
| commit | 7b9388b7b5fcdbb2f7e7178dc0a533e3284184c5 (patch) | |
| tree | 4933cdd8d33feb47f2c83461003f38516192f540 | |
| parent | d4ff949953141877743ee95123a492c4e48c3809 (diff) | |
| download | rust-7b9388b7b5fcdbb2f7e7178dc0a533e3284184c5.tar.gz rust-7b9388b7b5fcdbb2f7e7178dc0a533e3284184c5.zip | |
Explain that the tool is responsible for unknown tool_lints
| -rw-r--r-- | src/librustc/lint/levels.rs | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/librustc/lint/levels.rs b/src/librustc/lint/levels.rs index 6a29b8c3e3e..483e2ea8a96 100644 --- a/src/librustc/lint/levels.rs +++ b/src/librustc/lint/levels.rs @@ -273,9 +273,10 @@ impl<'a> LintLevelsBuilder<'a> { specs.insert(*id, (level, src)); } } - //FIXME: if Tool(None) is returned than the lint either does not exist in - //the lint tool or the code doesn't get compiled with the lint tool and - //therefore the lint cannot exist. + // If Tool(None) is returned, then either the lint does not exist in the + // tool or the code was not compiled with the tool and therefore the lint + // was never added to the `LintStore`. To detect this is the responsibility + // of the lint tool. } _ if !self.warn_about_weird_lints => {} |
