diff options
| author | Hugo Herbelin | 2019-05-08 21:28:25 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-05-14 11:15:15 +0200 |
| commit | 63a953ddc0db1ec1bf101ed6afdf9262d0d9f355 (patch) | |
| tree | b8b12986afa3c31115c57c66e69429047ce6667f /stm/asyncTaskQueue.ml | |
| parent | d452f359566ec6593aad564acb281f5a49dd931a (diff) | |
Ensuring suffix of file to compile also for -vio2vo checking.
We do it by consistently using variants of the "ensure_exists" policy
in compilation modes: vo (default), vio (-quick), vio2vo (-vio2vo) and
parallel vio2vo (schedule-vio2vo), vio checking (-check-vio-tasks) and
parallel vio checking (schedule-vio-checking).
For instance, coqc -vio2vo dir/file.vio now works, while before,
dir/file was expected.
Incidentally, this avoids the non-recommended Loadpath.locate_file.
Diffstat (limited to 'stm/asyncTaskQueue.ml')
0 files changed, 0 insertions, 0 deletions