# HG changeset patch
# User Gerd Moellmann <gerd@gnu.org>
# Date 989852069 0
# Node ID 1d2bd2c606e8362a2f7914700de74ebe40c475fe
# Parent  7e55768d52fd544416d312418195aaa1638d5597
(note_mouse_highlight): Avoid changing the mouse
pointer shape when show_mouse_face has already done it.

diff -r 7e55768d52fd -r 1d2bd2c606e8 src/xterm.c
--- a/src/xterm.c	Mon May 14 13:35:09 2001 +0000
+++ b/src/xterm.c	Mon May 14 14:54:29 2001 +0000
@@ -6997,6 +6997,7 @@
 
 	      /* Display it as active.  */
 	      show_mouse_face (dpyinfo, DRAW_MOUSE_FACE);
+	      cursor = None;
 	    }
 	  /* Handle the text property case.  */
 	  else if (!NILP (mouse_face) && BUFFERP (object))
@@ -7038,6 +7039,7 @@
 
 	      /* Display it as active.  */
 	      show_mouse_face (dpyinfo, DRAW_MOUSE_FACE);
+	      cursor = None;
 	    }
 	  else if (!NILP (mouse_face) && STRINGP (object))
 	    {
@@ -7069,6 +7071,7 @@
 		= face_at_string_position (w, object, pos, 0, 0, 0, &ignore,
 					   glyph->face_id, 1);
 	      show_mouse_face (dpyinfo, DRAW_MOUSE_FACE);
+	      cursor = None;
 	    }
 	}