From 51d4d83316f91abb25ea331bfdc1dcba17362dc8 Mon Sep 17 00:00:00 2001
From: Paul Steckler
Date: Tue, 15 Aug 2017 10:31:09 -0400
Subject: Add native compute profiling, BZ#5170

---
 vernac/vernacentries.ml | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

(limited to 'vernac')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 4f63ed6f48..8738e58e82 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1457,6 +1457,22 @@ let _ =
       optread  = CWarnings.get_flags;
       optwrite = CWarnings.set_flags }
 
+let _ =
+  declare_string_option 
+    { optdepr  = false;
+      optname  = "native_compute profiler output";
+      optkey   = ["NativeCompute"; "Profile"; "Filename"];
+      optread  = Nativenorm.get_profile_filename;
+      optwrite = Nativenorm.set_profile_filename }
+
+let _ =
+  declare_bool_option
+    { optdepr  = false;
+      optname  = "enable native compute profiling";
+      optkey   = ["NativeCompute"; "Profiling"];
+      optread  = Nativenorm.get_profiling_enabled;
+      optwrite = Nativenorm.set_profiling_enabled }
+
 let vernac_set_strategy locality l =
   let local = make_locality locality in
   let glob_ref r =
-- 
cgit v1.2.3