On Wed, 2010-12-22 at 18:13 +0100, Ingo Molnar wrote:
The double "%%" acts as an escape and simply prints "%" rather than
treating it as a format specifier.
I did this separately so that any arguments about individual usage
didn't sink the whole ship. Don't worry, you'll get your usage sites
very soon. :)