diff options
| author | Enrico Tassi | 2014-11-26 18:42:40 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2014-11-27 16:06:54 +0100 |
| commit | 61209f27eb26dcb04a7d5428b9f2ab7f65f73ac8 (patch) | |
| tree | 42637501f42a47cb9978663f37317b3e0a0d7b75 /kernel/nativecode.ml | |
| parent | 10af47a5790987ee5211bac88c3a16396f30bcb0 (diff) | |
STM: put hooks in key events to let plugins customize the feedback
The default hook value is the one used by CoqIDE
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions