mirror of
https://github.com/Mercury-Language/mercury.git
synced 2025-12-15 22:03:26 +00:00
541ab2829f
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.
37 lines
1.1 KiB
Plaintext
37 lines
1.1 KiB
Plaintext
#---------------------------------------------------------------------------#
|
|
# Copyright (C) 1997-1999 The University of Melbourne.
|
|
# This file may only be copied under the terms of the GNU General
|
|
# Public License - see the file COPYING in the Mercury distribution.
|
|
#---------------------------------------------------------------------------#
|
|
#
|
|
# init_grade_options.sh-subr:
|
|
# An `sh' subroutine for initializing grade-related options.
|
|
# Used by the `ml' and `mgnuc' scripts.
|
|
#
|
|
# The code here should be inserted before a script's option-parsing
|
|
# loop. The invoking script must define a DEFAULT_GRADE option.
|
|
#
|
|
#---------------------------------------------------------------------------#
|
|
|
|
asm_labels=true
|
|
non_local_gotos=true
|
|
global_regs=true
|
|
gc_method=conservative
|
|
profile_time=false
|
|
profile_calls=false
|
|
profile_memory=false
|
|
profile_deep=false
|
|
use_trail=false
|
|
use_minimal_model=false
|
|
stack_trace=false
|
|
require_tracing=false
|
|
low_level_debug=false
|
|
thread_safe=false
|
|
|
|
case $# in
|
|
0) set - "--grade $DEFAULT_GRADE" ;;
|
|
0) set - "--grade $DEFAULT_GRADE" "$@" ;;
|
|
esac
|
|
|
|
#---------------------------------------------------------------------------#
|