Imported Upstream version 8.3.pl2upstream/8.3.pl2

1 files changed, 13 insertions, 1 deletions

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 98ef2791..cce2319b 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -14,6 +14,7 @@
    for fast computation of bounded (31bits) integers */
 
 #include <stdio.h>
+#include <signal.h>
 #include "coq_gc.h"
 #include "coq_instruct.h"
 #include "coq_fix_code.h"
@@ -157,6 +158,12 @@ sp is a local copy of the global variable extern_sp. */
 #endif
 #endif
 
+/* For signal handling, we highjack some code from the caml runtime */
+
+extern intnat caml_signals_are_pending;
+extern intnat caml_pending_signals[];
+extern void caml_process_pending_signals(void);
+
 /* The interpreter itself */
 
 value coq_interprete
@@ -414,8 +421,13 @@ value coq_interprete
 	realloc_coq_stack(Coq_stack_threshold);
 	sp = coq_sp;
       }
+      /* We also check for signals */
+      if (caml_signals_are_pending) {
+	/* If there's a Ctrl-C, we reset the vm */
+	if (caml_pending_signals[SIGINT]) { coq_sp = coq_stack_high; }
+	caml_process_pending_signals();
+      }
       Next;
-      /* Fall through CHECK_SIGNALS */
 
       Instruct(APPTERM) {
 	int nargs = *pc++;