chiark / gitweb /
notation: fixes from paper markup of 389264b