Re: Time to merge scratch/correct-warning-pos into master, perhaps?

[Gregory Heytings]

> > > That's consistent with what was reported at the beginning of this 
> > > thread (~7% slowdown).  Byte compilation is expected to be slightly 
> > > slower with this change.
> >
> > But make check does a lot more than byte compilation, or am I missing 
> > something?
>
> Not much more, IME.

That's not what the numbers tell us (again 3b33a14380 vs 7922131bb2):

make -j1 check: 181s (69s byte-compilation, 112s execution) vs 162s (58s 
byte-compilation, 104s execution)
make -j4 check: 45s (17s byte-compilation, 28s execution) vs 40s (15s 
byte-compilation, 25s execution)
make -j8 check: 26s (9s byte-compilation, 17s execution) vs 23s (7s 
byte-compilation, 16s execution)

In short, the compilation time in make check is slower (which is 
expected), but the execution time in make check is also consistently ~7% 
slower.