#778: #772: this and various editorial comments lines
opened by thuchacz