hide fold icons in manual mode

This commit is contained in:
Fabian Jakobs 2011-12-13 16:48:13 +01:00
commit b6fbe5b6bb

View file

@ -370,6 +370,7 @@ bindDropdown("fontsize", function(value) {
bindDropdown("folding", function(value) {
env.editor.getSession().setFoldStyle(value);
env.editor.setShowFoldWidgets(value !== "manual");
});
bindDropdown("soft_wrap", function(value) {