diff --git a/servers/is/dmp.c b/servers/is/dmp.c
index 7a46b4837..15d57d250 100644
--- 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();