[m-rev.] for review: Generate better man pages.

[Peter Wang]

On Mon, 27 May 2019 15:29:00 +0000 (UTC), Julien Fischer <jfischer at opturion.com> wrote:
> 
> 
> On Mon, 27 May 2019, Peter Wang wrote:
> 
> > doc/make_manpage:
> >    Replace the old script with a new version written in awk.
> >
> >    The new output should be an improvement in these ways:
> >      - works for tools that use spaces for indentation instead of tabs
> >      - uses .TP for indenting text instead of monospace text with
> >        inconsistent leading spaces
> >      - option names are in bold
> >      - removes redundant blank lines
> >
> > doc/Mmakefile:
> >    Adjust command line to call the new make_manpage script.
> >
> > profiler/mercury_profile.m:
> >    Add "Name:" line to --help output for make_manpage to read.
> >
> > scripts/mtags.in:
> >    Add "Name:" line to --help output for make_manpage to read.
> >
> >    Delete initial blank line in help and usage text.
> >
> >    Delete stray full stop.
> >
> > scripts/mprof_merge_runs:
> > scripts/parse_ml_options.sh-subr.in:
> >    Simplify --help text for make_manpage.
> 
> That's fine.

Thanks, pushed with improvements to make_manpage.

Peter