Derk-Jan Hartman a9cdbcacb4 Add tooltip to annotation indicator ... In the past I had made the annotation indicators clickable, and your cursor will in this case navigate to the next annotation in editor. This was not really easily discoverable, so I have added a tooltip to make it slightly more discoverable. I also added a CSS line to prevent users from accidently selecting the text (or rather numbers) in this area, which I had noticed happened to me at times when trying to click it. Change-Id: I47ecba232ff925169d0f64d85ae34ff6564cc1a5		2015-05-25 11:07:41 +02:00
..
ace	Ace: Update to 2015-01-28	2015-01-28 11:04:27 -08:00
ext.codeEditor.geshi.css	CodeEditor: Keep experimental Geshi editor working	2014-08-28 19:41:19 +00:00
ext.codeEditor.geshi.js	Merge "Use mediawiki.api.parse"	2014-10-16 17:16:42 +00:00
ext.codeEditor.js	Update formatting of JavaScript files	2013-12-31 13:03:11 +01:00
jquery.codeEditor.css	Add tooltip to annotation indicator	2015-05-25 11:07:41 +02:00
jquery.codeEditor.js	Add tooltip to annotation indicator	2015-05-25 11:07:41 +02:00