diff options
| author |  Hendrik Tews <hendrik@askra.de> | 2016-11-23 21:08:26 +0100 |
|---|---|---|
| committer | Hendrik Tews <hendrik@askra.de> | 2016-11-29 23:47:23 +0100 |
| commit | 1466839c2182b76853380a7c91e86af30fd9778f (patch) | |
| tree | 34ecbbb95902747a389674cbc8acfe30814645fc /doc/ProofGeneral.texi | |
| parent | d33897df4d6a2af94d0d315707111528a3c4a403 (diff) | |
support vio2vo background processing
Selecting quick-and-vio2vo will start vio2vo conversion in the
background on a subset of the available cores, see
`coq-max-background-vio2vo-percentage'. The vio2vo conversion
starts after all compilation for the require command has been
finished and the require has been processed. Because of a certain
incompatibility between .vio and .vo files (see coq issue 5223)
slowly single stepping through require commands does not
work (but processing them as a batch does).
Diffstat (limited to 'doc/ProofGeneral.texi')
0 files changed, 0 insertions, 0 deletions