add CHANGES entry

1 files changed, 4 insertions, 0 deletions

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