diff options
Diffstat (limited to 'byterun/intern.c')
| -rw-r--r-- | byterun/intern.c | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/byterun/intern.c b/byterun/intern.c index 35d293b60..713f1feaa 100644 --- a/byterun/intern.c +++ b/byterun/intern.c @@ -126,7 +126,10 @@ static void intern_rec(value *dest) header_t header; char cksum[16]; struct custom_operations * ops; + value * function_placeholder; + int get_function_placeholder; + get_function_placeholder = 1; tailcall: code = read8u(); if (code >= PREFIX_SMALL_INT) { @@ -311,6 +314,15 @@ static void intern_rec(value *dest) ofs = read32u(); readblock(cksum, 16); if (memcmp(cksum, caml_code_checksum(), 16) != 0) { + if (get_function_placeholder) { + function_placeholder = + caml_named_value ("Debugger.function_placeholder"); + get_function_placeholder = 0; + } + if (function_placeholder != NULL) { + v = *function_placeholder; + break; + } intern_cleanup(); caml_failwith("input_value: code mismatch"); } |