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

[Julien Fischer]

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.

Julien.