aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/nativeconv.ml
diff options
context:
space:
mode:
authorGravatar Paul Steckler <steck@stecksoft.com>2017-08-15 10:31:09 -0400
committerGravatar Paul Steckler <steck@stecksoft.com>2017-08-17 11:40:26 -0400
commit51d4d83316f91abb25ea331bfdc1dcba17362dc8 (patch)
tree25eb115f4faeb87d6ae0d3db687f3111fdcf1886 /kernel/nativeconv.ml
parent63da901edc3ab5b69098499cdc01ab50ed9b3353 (diff)
Add native compute profiling, BZ#5170
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 d2f050d3b..a62a079da 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -132,7 +132,7 @@ let native_conv_gen pb sigma env univs t1 t2 =
let penv = Environ.pre_env env in
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
+ match compile ml_filename code ~profile:false with
| (true, fn) ->
begin
if !Flags.debug then Feedback.msg_debug (Pp.str "Running test...");