From ce83c2b9fd1685e46049ee7f47c8716dcf66dbd1 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 6 Oct 2015 14:11:19 +0200
Subject: Goptions: new value type: optional string

These options can be set to a string value, but also unset.
Internal data is of type string option.
---
 ide/interface.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'ide/interface.mli')

diff --git a/ide/interface.mli b/ide/interface.mli
index 464e851f6d..767c49d2bd 100644
--- a/ide/interface.mli
+++ b/ide/interface.mli
@@ -61,6 +61,7 @@ type option_value =
   | BoolValue   of bool
   | IntValue    of int option
   | StringValue of string
+  | StringOptValue of string option
 
 (** Summary of an option status *)
 type option_state = {
-- 
cgit v1.2.3