diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-08-29 17:13:03 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-08-29 17:13:03 +0200 |
| commit | f1806ab001cfbc9548e607397fc55b9c1be7c25b (patch) | |
| tree | 9a14f5bc56e4ad19b977f6606ff86d86d8d892d7 /CHANGES | |
| parent | f67ebbba77998e6469ad0fc9dc80b306ab2e62ce (diff) | |
| parent | c62a286bad2ec0ced1e7b5e8987f5f7e476ab11c (diff) | |
Merge PR #950: Rudimentary support for native_compute profiling, BZ#5170
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 |