diff options
| author |  Hendrik Tews <hendrik@askra.de> | 2016-12-08 16:06:17 +0100 |
|---|---|---|
| committer | Hendrik Tews <hendrik@askra.de> | 2016-12-08 16:06:17 +0100 |
| commit | 687e008bc80ca6f66ca8920296c2e8dab889c752 (patch) | |
| tree | 970bed3af3a948a02eb19502c45763eb75e984c5 /doc | |
| parent | cde8f9e4a13ec2d05c8435be16da02e54e6b5a70 (diff) | |
option coq-compile-keep-going for parallel compilation
With this option set, compilation continues after the first error
to compile as much as possible and to potentially report more
than one error.
Diffstat (limited to 'doc')
0 files changed, 0 insertions, 0 deletions