diff options
Diffstat (limited to 'ide/protocol/interface.ml')
| -rw-r--r-- | ide/protocol/interface.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/ide/protocol/interface.ml b/ide/protocol/interface.ml index 362833743e..be5e305ad3 100644 --- a/ide/protocol/interface.ml +++ b/ide/protocol/interface.ml @@ -71,8 +71,6 @@ type option_state = { (** Whether an option is synchronous *) opt_depr : bool; (** Whether an option is deprecated *) - opt_name : string; - (** A short string that is displayed when using [Test] *) opt_value : option_value; (** The current value of the option *) } |