aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/nativeconv.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/nativeconv.ml')
-rw-r--r--kernel/nativeconv.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index c7701a8b1..04747cd8b 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -135,7 +135,7 @@ let native_conv pb sigma env t1 t2 =
let ml_filename, prefix = get_ml_filename () in
let code, upds = mk_conv_code penv sigma prefix t1 t2 in
match compile ml_filename code with
- | (0,fn) ->
+ | (true, fn) ->
begin
if !Flags.debug then Pp.msg_debug (Pp.str "Running test...");
let t0 = Sys.time () in