From 5cc99c019d91d691e7d6441a0ecaa881b091abe7 Mon Sep 17 00:00:00 2001 From: Matthew Flatt Date: Thu, 9 Dec 2010 17:38:20 -0700 Subject: [PATCH] win32: fix delete key Closes PR 11519 original commit: b16f8fb16a7efe9e62e6cb9d20aafe15c6a7d9b8 --- collects/mred/private/wx/win32/key.rkt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/collects/mred/private/wx/win32/key.rkt b/collects/mred/private/wx/win32/key.rkt index a34a6760..4bb96647 100644 --- a/collects/mred/private/wx/win32/key.rkt +++ b/collects/mred/private/wx/win32/key.rkt @@ -70,7 +70,7 @@ VK_PRINT 'print VK_EXECUTE 'execute VK_INSERT 'insert - VK_DELETE 'delete + VK_DELETE #\rubout VK_HELP 'help VK_NUMPAD0 'numpad0 VK_NUMPAD1 'numpad1