Fixes issues with editor settings not working when changed, as discussed in #280 and #281.
With this changeset, the IDE options in Settings > General for JavaScript editor keymap, theme, indentation type and size, and code hints should now take effect immediately when changed and should be remembered when the page is reloaded.
gfwilliams
commented
1 year ago
Fixes issues with editor settings not working when changed, as discussed in #280 and #281.
With this changeset, the IDE options in Settings > General for JavaScript editor keymap, theme, indentation type and size, and code hints should now take effect immediately when changed and should be remembered when the page is reloaded.