diff options
| author | Hendrik Tews | 2016-11-22 23:06:30 +0100 |
|---|---|---|
| committer | Hendrik Tews | 2016-11-22 23:07:29 +0100 |
| commit | d33897df4d6a2af94d0d315707111528a3c4a403 (patch) | |
| tree | 3e8837c6142f27f9ca86c414ba1b971492fa9273 /pgshell/pgshell.el | |
| parent | c4caac41845362173499397e589e9619f5e18d77 (diff) | |
improve compilation when both .vio and .vo are up-to-date
In this case Coq loads the younger file and emits a warning if
the .vio file is the younger one. With this patch, the dependency
analysis for parallel compilation continues with the older value.
The interesting case to look at is when b.v depends on a.v and
both are compiled with -quick and later a parallel vio2vo
produces a.vo and b.vo such that b.vo is older (because, eg. b.v
is shorter than a.v). Without this patch a second auto
compilation would recompile b.v, because the dependency a.vo is
younger.
Diffstat (limited to 'pgshell/pgshell.el')
0 files changed, 0 insertions, 0 deletions
