diff options
| author | Théo Zimmermann | 2019-02-26 16:33:08 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-02-28 14:26:41 +0100 |
| commit | 9c201fe42142de7332149863d6c1343c2dec8391 (patch) | |
| tree | c97b2599ade286f79c88d07f335f215112fc0018 /dev/doc/debugging.md | |
| parent | 9d6f268723b6352a97bcc3baf0df57f1c1b251fa (diff) | |
[sphinx] Add warn option to coqtop directive.
By default Coq warnings are made fatal when building the manual.
If you want to show a command resulting in a warning, use the warn
option.
Preexisting warnings are either fixed or marked as expected.
Diffstat (limited to 'dev/doc/debugging.md')
0 files changed, 0 insertions, 0 deletions