mirror of
https://github.com/Mercury-Language/mercury.git
synced 2025-12-14 05:12:33 +00:00
Estimated hours taken: 0.5 Add a new option for deep profiling to the compiler and the scripts. compiler/options.m: Add the new profiling options `profile-deep' and `deep-profiling'. compiler/handle_options.m: Add code to handle the above options. scripts/init_grade_options.sh-subr: Initialize the profile_deep option to false. scripts/parse_grade_options.sh-subr: Add code handle the deep-profiling options.