Retire use of rman and instead use a custom man formatter. Rman did a bad job with some pages (e.g. ‘stat’) and it is regularly moved around (it is part of the dev. tools but “private”). Changed: U trunk/Support/bin/html_man.sh A trunk/Support/bin/man2html