Files
mercury/profiler
Peter Wang 10d29a489a Generate better man pages.
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 macros for indenting proportional font 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.

compiler/options.m:
    Minor formatting changes to --help text to keep complexity of
    make_manpage script low.

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.
2019-05-28 15:54:45 +10:00
..
2019-05-28 15:54:45 +10:00
2018-01-09 01:05:42 +11:00