diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2015-10-14 17:23:27 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2015-10-15 14:36:30 +0200 |
commit | d08aa6b4f742a7162e726920810765258802c176 (patch) | |
tree | e1cca6b452cdbebb79d0ef9d4bd45693ccfd1bbd /kernel | |
parent | 7ae876ab6246a9c9d352b7c72d3f98db47ff456c (diff) |
Warn user when bytecode compilation fails.
Previously, the kernel was silently switching back to the standard conversion.
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/reduction.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 9479e38ca..0f105b048 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -735,8 +735,9 @@ let vm_conv cv_pb env t1 t2 = try !vm_conv cv_pb env t1 t2 with Not_found | Invalid_argument _ -> - (* If compilation fails, fall-back to closure conversion *) - fconv cv_pb false (fun _->None) env t1 t2 + (Pp.msg_warning + (Pp.str "Bytecode compilation failed, falling back to default conversion"); + fconv cv_pb false (fun _->None) env t1 t2) let default_conv cv_pb ?(l2r=false) env t1 t2 = fconv cv_pb false (fun _ -> None) env t1 t2 |