diff options
Diffstat (limited to 'ide/utils/configwin.ml')
| -rw-r--r-- | ide/utils/configwin.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/ide/utils/configwin.ml b/ide/utils/configwin.ml index 275d8616..05bf54eb 100644 --- a/ide/utils/configwin.ml +++ b/ide/utils/configwin.ml @@ -43,9 +43,7 @@ class key_cp = Configwin_types.key_cp let string = Configwin_ihm.string -let custom_string = Configwin_ihm.custom_string let text = Configwin_ihm.text -let custom_text = Configwin_ihm.custom_text let strings = Configwin_ihm.strings let list = Configwin_ihm.list let bool = Configwin_ihm.bool |