Merge pull request #6333 from github/rc/3.2

Merge rc/3.2 to main
This commit is contained in:
Arthur Baars
2021-07-20 12:19:20 +02:00
committed by GitHub
2 changed files with 16 additions and 0 deletions

View File

@@ -14,6 +14,14 @@
problem.severity:
- error
- warning
- include:
kind:
- diagnostic
- include:
kind:
- metric
tags contain:
- summary
- exclude:
deprecated: //
- exclude:

View File

@@ -19,6 +19,14 @@
- warning
tags contain:
- security
- include:
kind:
- diagnostic
- include:
kind:
- metric
tags contain:
- summary
- exclude:
deprecated: //
- exclude: