Commit 3c978d34 "fixed" a whitespace issue by replacing two consecutive
space characters in a format string by a single space. However,
the duplicated space character actually had a purpose. This commit
re-adds the additional space character and explains through a comment
why it is needed.