diff options
| author | Emilio Jesus Gallego Arias | 2017-11-06 14:52:12 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-11-06 14:55:21 +0100 |
| commit | 4197eb4f94f0bd57b4e9cd391a19968eed373a0d (patch) | |
| tree | 0087e7eb7d8bdc137c922aa923928e98ba724b06 /ide/FAQ | |
| parent | e029cf5b417b22ebc65a8193469bbbe450f725ce (diff) | |
[feedback] Helper to print feedback messages in the console.
This is useful for tools such as `coqchk` or `coq_makefile` that want
to handle feedback on their own.
Diffstat (limited to 'ide/FAQ')
0 files changed, 0 insertions, 0 deletions