Skip to content

Commit

Permalink
bugfix: don't warn about 'trusted' attribute; fixes #1324
Browse files Browse the repository at this point in the history
  • Loading branch information
tjhance committed Oct 29, 2024
1 parent 48187c7 commit 888c93a
Showing 1 changed file with 1 addition and 0 deletions.
1 change: 1 addition & 0 deletions source/rust_verify/src/attributes.rs
Original file line number Diff line number Diff line change
Expand Up @@ -922,6 +922,7 @@ pub(crate) fn get_external_attrs(
Attr::VerusMacro => es.verus_macro = true,
Attr::SizeOfGlobal => es.size_of_global = true,
Attr::InternalGetFieldManyVariants => es.internal_get_field_many_variants = true,
Attr::Trusted => {}
Attr::UnsupportedRustcAttr(..) => {}
_ => {
es.any_other_verus_specific_attribute = true;
Expand Down

0 comments on commit 888c93a

Please sign in to comment.