changeset 42540:b575cbf7f94e

(w32_menu_display_help): Hide any tooltip window.
author Jason Rumney <jasonr@gnu.org>
date Sat, 05 Jan 2002 00:14:57 +0000
parents 90ad1db5d8f3
children 8c7aa169a6ae
files src/w32menu.c
diffstat 1 files changed, 2 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/src/w32menu.c	Sat Jan 05 00:09:08 2002 +0000
+++ b/src/w32menu.c	Sat Jan 05 00:14:57 2002 +0000
@@ -2226,6 +2226,8 @@
 	 Windows code on the non-toolkit version.  */
       if (f)
 	{
+	  Fx_hide_tip ();
+
 	  XSETFRAME (frame, f);
 	  kbd_buffer_store_help_event (frame, help);
 	}