diff options
| author | Enrico Tassi | 2021-01-06 17:14:22 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2021-01-27 09:45:49 +0100 |
| commit | 2caae4d530ba97ced98711986dc504f9becdab81 (patch) | |
| tree | 7447cc86cea8c175449a86b695998e78586ee880 /sysinit | |
| parent | f5ec3f5cbd4bc2e0f65e1c52143b199ce7c2a5ad (diff) | |
[coqargs] use standard option injection for -mangle-names
Diffstat (limited to 'sysinit')
| -rw-r--r-- | sysinit/coqargs.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml index 19350b7e98..ac9e430d31 100644 --- a/sysinit/coqargs.ml +++ b/sysinit/coqargs.ml @@ -348,9 +348,8 @@ let parse_args ~usage ~init arglist : t * string list = add_load_vernacular oval true (next ()) |"-mangle-names" -> - Goptions.set_bool_option_value ["Mangle"; "Names"] true; - Goptions.set_string_option_value ["Mangle"; "Names"; "Prefix"] (next ()); - oval + let oval = add_set_option oval ["Mangle"; "Names"] (OptionSet None) in + add_set_option oval ["Mangle"; "Names"; "Prefix"] (OptionSet(Some(next ()))) |"-profile-ltac-cutoff" -> Flags.profile_ltac := true; |