# HG changeset patch
# User wenzelm
# Date 1396614691 -7200
# Node ID 0e21270952c319658a51d833f2e78f213f9d8dd5
# Parent  954d5be07d205337e57826a6643bb856098eccb9
revert ce37fcb30cf2 for the sake of Mac OS X -- let some event listeners of jEdit reset the cursor;

diff -r 954d5be07d20 -r 0e21270952c3 src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Fri Apr 04 13:12:16 2014 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Fri Apr 04 14:31:31 2014 +0200
@@ -122,7 +122,7 @@
           if (new_text_info.isDefined)
             text_area.getPainter.setCursor(Cursor.getPredefinedCursor(cursor.get))
           else
-            text_area.getPainter.setCursor(Cursor.getPredefinedCursor(Cursor.TEXT_CURSOR))
+            text_area.getPainter.resetCursor()
         }
         for {
           r0 <- JEdit_Lib.visible_range(text_area)