diff options
| author | Gaëtan Gilbert | 2019-05-28 17:25:58 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-05-28 18:49:03 +0200 |
| commit | 356f496f16219c5e3bd9a651b867c48411bde17d (patch) | |
| tree | d559813a8e7a00effa672dea7b5df9d70a199f43 /doc/plugin_tutorial | |
| parent | be21788fc5cbe86af52d4f0ea21daa73ed8fcf4f (diff) | |
Fix printers.sh test when missing coqtop.byte, print more info
Diffstat (limited to 'doc/plugin_tutorial')
0 files changed, 0 insertions, 0 deletions