mirror of
https://github.com/Mercury-Language/mercury.git
synced 2025-12-18 23:35:25 +00:00
Estimated hours taken: 2 scripts/mprof_merge_runs: New file. A script for merging multiple runs into a single profile. scripts/Mmakefile: Add mprof_merge_runs to the list of scripts. doc/Mmakefile: Add mprof_merge_runs to the list of things which need manpages. (The manpage will be created automatically by `make_manpage'.) doc/user_guide.texi: Document the use of mprof_merge_runs.