added buttons to manage editor font-size

2013-06-13 22:56:01 +02:00
parent ebc27cbc46
commit 234c926d98
3 changed files with 33 additions and 1 deletions
@@ -122,7 +122,7 @@
 		jQuery("#{{=id}} textarea").data('editor', editor);
 		var hlLine = editor.addLineClass(0, "background", "activeline");
 		window.mirror = editor; 	//backward compatibility
-
+		set_font(editor, current_font_incr);
 		doListBreakpoints({{=XML("'%s','%s://%s%s'" % (filename, 
 				request.env['wsgi_url_scheme'], request.env['http_host'],
 				URL(c='debug', f='list_breakpoints')))}}, editor);