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