* Fix for gutter line highlighting setting

This commit is contained in:
Ruben Daniels 2012-05-04 22:47:01 -07:00
commit 580c290971

View file

@ -878,6 +878,7 @@ var Editor = function(renderer, session) {
return;
this.renderer.setHighlightGutterLine(shouldHighlight);
this.$highlightGutterLine = shouldHighlight;
};
this.getHighlightGutterLine = function() {