We were printing any non-argument-consuming parts of printf format strings literally, but that is not right: printf("%%") is supposed to print "%", not "%%".
Description of change
We have already checked the format string, we already know that the format string consumes no arguments, so just pass it to printf to handle any embedded %%.
Anything else we should know?
If there's any other relevant information we should know that may help us in
understanding and verifying your patch, please include it here.
Overview
Fix printf of %%.
Reason for change
We were printing any non-argument-consuming parts of printf format strings literally, but that is not right: printf("%%") is supposed to print "%", not "%%".
Description of change
We have already checked the format string, we already know that the format string consumes no arguments, so just pass it to printf to handle any embedded %%.
Anything else we should know?
If there's any other relevant information we should know that may help us in understanding and verifying your patch, please include it here.
Checklist