I thought the policy for example comments "// OK, explanation" was to use a comma. However, the statistics are not in my favor: ``` $ grep "// OK," *.tex | wc -l 138 $ grep "// OK:" *.tex | wc -l 251 ``` Asking for confirmation of the policy before providing a large-scale fix. Incidentally related to #3126.