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

[Gregory Heytings]

> > > However the bootstrap is still faster than it was this time last week, 
> > > due to commit 10083e788f7349fa363d100687dc3d94bea88f57 on Thursday.
> >
> > That is only true for those who use --with-native-compilation.  I 
> > don't.
>
> It's supposed to be faster even without native compilation, albeit 
> perhaps not by the same amount.

I don't know, but I just compared 7922131bb2 vs 3b33a14380, and in most 
cases 7922131bb2 is even a bit slower than correct-warning-pos:

make -j1 bootstrap: 654s vs 596s
make -j4 bootstrap: 256s vs 238s
make -j8 bootstrap: 201s vs 183s

make -j1 check: 181s vs 162s
make -j4 check: 45s vs 40s
make -j8 check: 26s vs 23s