diff options
Diffstat (limited to 'maint')
| -rwxr-xr-x | maint/add_warning | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/maint/add_warning b/maint/add_warning index a86caa357..3a3dcc4f9 100755 --- a/maint/add_warning +++ b/maint/add_warning @@ -43,6 +43,7 @@ WANT_LINTS = """ #![warn(clippy::unseparated_literal_suffix)] #![deny(clippy::unwrap_used)] #![allow(clippy::let_unit_value)] // This can reasonably be done for explicitness +#![allow(clippy::uninlined_format_args)] #![allow(clippy::significant_drop_in_scrutinee)] // arti/-/merge_requests/588/#note_2812945 #![allow(clippy::result_large_err)] // temporary workaround for arti#587 """ @@ -57,6 +58,7 @@ TEST_LINTS = """ #![allow(clippy::print_stdout)] #![allow(clippy::single_char_pattern)] #![allow(clippy::unwrap_used)] +#![allow(clippy::unchecked_duration_subtraction)] """ # ---------- some notes about lints we might use - NOT USED by any code here ---------- |
