[devel] Minor editing of the manual.
4 files changed