Tag: info-document-has-wrong-extension
Severity: warning
Check: documentation/texinfo
Explanation: The info document has an extension other than info*.gz.