aboutsummaryrefslogtreecommitdiff
path: root/pgshell/pgshell.el
diff options
context:
space:
mode:
authorHendrik Tews2016-11-22 23:06:30 +0100
committerHendrik Tews2016-11-22 23:07:29 +0100
commitd33897df4d6a2af94d0d315707111528a3c4a403 (patch)
tree3e8837c6142f27f9ca86c414ba1b971492fa9273 /pgshell/pgshell.el
parentc4caac41845362173499397e589e9619f5e18d77 (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