412601690e
This removes redundant inline docs, because - users should consult the better docs in the manual, - contributors should add to the manual, not the inline comments