mirror of
https://github.com/Mercury-Language/mercury.git
synced 2025-12-21 00:39:37 +00:00
Turn off value_number by default for everyone else.
This commit is contained in:
@@ -186,8 +186,8 @@ option_defaults_2(optimization_option, [
|
||||
optimize_peep - bool(yes),
|
||||
optimize_jumps - bool(yes),
|
||||
optimize_labels - bool(yes),
|
||||
optimize_value_number - bool(yes),
|
||||
optimize_frames - bool(no),
|
||||
optimize_value_number - bool(no),
|
||||
optimize_frames - bool(yes),
|
||||
optimize_repeat - int(4),
|
||||
static_ground_terms - bool(yes),
|
||||
smart_indexing - bool(yes),
|
||||
|
||||
Reference in New Issue
Block a user