On Thu, 23 Apr 1998, Mark Brinicombe wrote:
> This fixes PR port-arm32/5178 and as soon as I am happy that it is stable
> I will commit it. I have been hammering machines with the patches and
> things appear stable so if folks would like to test it as well that would
> be great ;-)

It seems to be working.... I also get a slight speed-up on 'make includes'
in /usr/src/bin, from 50s real, 28s user, 21 system down to 44/28/14; so
its comforting to know its actually made a difference :-)

-- 
alex@hayward.u-net.com; xelah@ferret.lmh.ox.ac.uk