No more F9

diff --git a/servers/is/dmp.c b/servers/is/dmp.c
index 7a46b483738a3ef554c51e1140317a5e9bc0421c..15d57d250123cb7c2d00e4048ecf013545ed9cbc 100644 (file)
--- a/servers/is/dmp.c
+++ b/servers/is/dmp.c
@@ -40,18 +40,6 @@ PUBLIC int do_fkey_pressed(message *m)
   if (pressed(F11))    timing_dmp();
   if (pressed(F12))    sched_dmp();
 
-  if (pressed(F9)) { 
-       printf("IS server going into infinite loop... hit 5x a function key\n");
-       printf("Five times a function key is fine as well ...\n");
-       while(TRUE) {
-               if (OK == nb_receive(ANY, m)) {
-                       if (s++ >= 5 ) break;
-               }
-       }
-       printf("IS server back to normal ... \n");
-       return(EDONTREPLY);
-  }
-
   /* Also check Shift F1-F6 keys. */
   if (pressed(SF1))    mproc_dmp();
   if (pressed(SF2))    sigaction_dmp();