-- In a root module, the filename is allowed to diverge from the module
-- name, so we have to check that there aren't multiple root files
-- In a root module, the filename is allowed to diverge from the module
-- name, so we have to check that there aren't multiple root files