aboutsummaryrefslogtreecommitdiff
path: root/stm/asyncTaskQueue.ml
diff options
context:
space:
mode:
authorThéo Zimmermann2020-04-01 16:54:37 +0200
committerThéo Zimmermann2020-04-06 15:30:08 +0200
commit5c5fbf68034fdd18ddfcd19c9c8b1438af6b5c92 (patch)
tree32313fbf73082cff3da3832b0ff709c192ec28b7 /stm/asyncTaskQueue.ml
parent2089207415565e8a28816f53b61d9292d04f4c59 (diff)
Clean and fix definitions of options.
- Provide new helper functions in `Goptions` on the model of `declare_bool_option_and_ref`; - Use these helper functions in many parts of the code base (encapsulates the corresponding references); - Move almost all options from `declare_string_option` to `declare_stringopt_option` (only "Warnings" continue to use the former). This means that these options now support `Unset` to get back to the default setting. Note that there is a naming misalignment since `declare_int_option` is similar to `declare_stringopt_option` and supports `Unset`. When "Warning" is eventually migrated to support `Unset` as well, we can remove `declare_string_option` and rename `declare_stringopt_option` to `declare_string_option`. - For some vernac options and flags that have an equivalent command-line option or flag, implement it like the standard `-set` and `-unset`.
Diffstat (limited to 'stm/asyncTaskQueue.ml')
0 files changed, 0 insertions, 0 deletions