diff options
| author | Emilio Jesus Gallego Arias | 2019-02-14 13:10:08 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-04-24 14:01:11 +0200 |
| commit | ed1b663afdd02355877c51dc9c759ddfd91b0854 (patch) | |
| tree | fe94e5bebe4455ad7dbf613d03fc9ca1385ce940 /doc/plugin_tutorial/tuto1 | |
| parent | 75c5264aa687480c66a6765d64246b5ebd2c0d54 (diff) | |
[proof] Fix proof bullet error helper which was implemented as a hook
We add the information on the proper layer by catching the low-level
exception.
Diffstat (limited to 'doc/plugin_tutorial/tuto1')
0 files changed, 0 insertions, 0 deletions