diff options
Diffstat (limited to 'ide/preferences.mli')
| -rw-r--r-- | ide/preferences.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/ide/preferences.mli b/ide/preferences.mli index 2094443b4..6ee7918fe 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -49,7 +49,6 @@ type pref = mutable window_height : int; mutable query_window_width : int; mutable query_window_height : int; - mutable fold_delay_ms : int; (* mutable use_utf8_notation : bool; *) |