diff options
| author | Pierre Roux | 2019-04-05 12:49:53 +0200 |
|---|---|---|
| committer | Pierre Roux | 2019-04-30 08:22:19 +0200 |
| commit | e9fec7c112a7792d67949ef5abe3de8a8832beda (patch) | |
| tree | 8d43c97946774b2a6eb63ac1f8d4288eb3e5ba91 /kernel | |
| parent | df6328178a92d7a51e2a08acbec5013d080e73aa (diff) | |
[vm] Backport from OCaml
Backport
https://github.com/ocaml/ocaml/commit/71b94fa3e8d73c40e298409fa5fd6501383d38a6
and
https://github.com/ocaml/ocaml/commit/d3e86fdfcc8f40a99380303f16f9b782233e047e
from OCaml VM
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/byterun/coq_interp.c | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index a8fd2fbe47..da152599ce 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -104,7 +104,8 @@ if (sp - num_args < coq_stack_threshold) { \ several architectures. */ -#if defined(__GNUC__) && !defined(DEBUG) +#if defined(__GNUC__) && !defined(DEBUG) && !defined(__INTEL_COMPILER) \ + && !defined(__llvm__) #ifdef __mips__ #define PC_REG asm("$16") #define SP_REG asm("$17") |