# HG changeset patch
# User wenzelm
# Date 1396283315 -7200
# Node ID ce37fcb30cf23600818ed6a5e03d661e5cda4c1c
# Parent  f968f4e3d5201640ae738fe3dc2cbf29d592f31e
reset mouse pointer more decisively, for the sake of Mac OS X (despite the builtin policie of jEdit);

diff -r f968f4e3d520 -r ce37fcb30cf2 src/Tools/jEdit/src/rich_text_area.scala
--- 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)