From a41397add86764abac1a087e1692b29cec3ad3ab Mon Sep 17 00:00:00 2001
From: Paul Steckler
Date: Thu, 17 Aug 2017 12:02:46 -0400
Subject: add CHANGES entry

---
 CHANGES | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/CHANGES b/CHANGES
index ed2f172067..1dbf4c64c1 100644
--- a/CHANGES
+++ b/CHANGES
@@ -63,6 +63,10 @@ Tactics
   Ltac definition or a Tactic Notation.
 - New option `Set Ltac Batch Debug` on top of `Set Ltac Debug` for
   non-interactive Ltac debug output.
+- On Linux, "native_compute" calls can be profiled using the "perf"
+  utility. The command "Set NativeCompute Profiling" enables
+  profiling, and "Set NativeCompute Profile Filename" customizes
+  the profile filename.
 
 Gallina
 
-- 
cgit v1.2.3