diff options
| author | Enrico Tassi | 2021-01-26 13:24:25 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2021-01-26 15:27:22 +0100 |
| commit | df3cbbee21cfaf03f7c2b9bd78280f25a5512f5a (patch) | |
| tree | d411c147cf77178cd4ec94183e441da471acd0e7 /stm/stm.mli | |
| parent | 0a6444c522c18c634fe1030436ea82f326bada9a (diff) | |
[options] improve support for append
Diffstat (limited to 'stm/stm.mli')
| -rw-r--r-- | stm/stm.mli | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/stm/stm.mli b/stm/stm.mli index 097bcbe0ca..e0c33a309b 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -52,7 +52,10 @@ type stm_doc_type = | VioDoc of string (* file path *) | Interactive of interactive_top (* module path *) -type option_command = OptionSet of string option | OptionUnset +type option_command = + | OptionSet of string option + | OptionAppend of string + | OptionUnset type injection_command = | OptionInjection of (Goptions.option_name * option_command) |