//@ ignore-auxiliary (used by `./mod_file_disambig.rs`)