diff --git a/build_support/boot_textarea.js b/build_support/boot_textarea.js index 16cb6c50..111a6043 100644 --- a/build_support/boot_textarea.js +++ b/build_support/boot_textarea.js @@ -424,6 +424,7 @@ function setupSettingPanel(settingDiv, settingOpener, api, options) { gutter: BOOL, fontSize: { "10px": "10px", + "11px": "11px", "12px": "12px", "14px": "14px", "16px": "16px"