changeset 56339 | ce37fcb30cf2 |
parent 56322 | f9ad26836516 |
child 56340 | af8cb60b55eb |
--- a/src/Tools/jEdit/src/rich_text_area.scala Mon Mar 31 17:41:45 2014 +0200 +++ b/src/Tools/jEdit/src/rich_text_area.scala Mon Mar 31 18:28:35 2014 +0200 @@ -122,7 +122,7 @@ if (new_text_info.isDefined) text_area.getPainter.setCursor(Cursor.getPredefinedCursor(cursor.get)) else - text_area.getPainter.resetCursor + text_area.getPainter.setCursor(Cursor.getPredefinedCursor(Cursor.TEXT_CURSOR)) } for { r0 <- JEdit_Lib.visible_range(text_area)