Fabian Jakobs aa03a915f7 use the same font for the gutter and the editor		2011-07-28 14:37:28 +02:00
..
ace	use the same font for the gutter and the editor	2011-07-28 14:37:28 +02:00