diff options
| author |  Paul Steckler <steck@stecksoft.com> | 2017-08-17 12:02:46 -0400 |
|---|---|---|
| committer | Paul Steckler <steck@stecksoft.com> | 2017-08-18 17:09:12 -0400 |
| commit | a41397add86764abac1a087e1692b29cec3ad3ab (patch) | |
| tree | 1b66f389aad21323f8ebeadc465aedfc64fe3940 /CHANGES | |
| parent | 3f4963f4523bbc4a079a7669de3a3fb3126f3a2a (diff) | |
add CHANGES entry
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 4 |
1 files changed, 4 insertions, 0 deletions
@@ -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 |