chiark / gitweb /
doc: Fix a formatting bug