comparison src/.gdbinit @ 37726:1d2bd2c606e8

(note_mouse_highlight): Avoid changing the mouse pointer shape when show_mouse_face has already done it.
author Gerd Moellmann <gerd@gnu.org>
date Mon, 14 May 2001 14:54:29 +0000
parents f440b9766968
children d2dfa348e7d8
comparison
equal deleted inserted replaced
37725:7e55768d52fd 37726:1d2bd2c606e8