diff options
| author | Gaëtan Gilbert | 2019-04-24 13:56:25 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-04-24 14:01:11 +0200 |
| commit | 7fd23f30ef6c52aabc8d1084171d906e1080f3f2 (patch) | |
| tree | ec73c181399217e12f56d77c868d7b8d4be82382 /doc/plugin_tutorial/tuto1/src | |
| parent | ed1b663afdd02355877c51dc9c759ddfd91b0854 (diff) | |
Fix proof bullet error helper (nosuchgoal)
The [int] is incorrect for list focusing, we could work a bit harder
to fix that. It's only used for pluralisation in the error message "no
such goal(s)" so we could also ignore the issue.
Diffstat (limited to 'doc/plugin_tutorial/tuto1/src')
0 files changed, 0 insertions, 0 deletions