//@ ignore-auxiliary (used by `../attributes-on-modules-fail.rs`)