Patch: Fix for bootstrap/3075

[Tom Tromey]

Rainer> Still fails the same way.

Thanks.

I'll write a real fix and test it here.  Then I'll resubmit it.  This
will take a few hours.

Tom