Re: build.sh trying to write to source tree

> OK, can you see if you can reproduce it after removing (or renaming)
> $OBJDIR/tools/what ?
Oops, that didn't exist (and ran build-sh -o).
I omitted the -o and now it probably works (for reasons unknown, it seems to 
have decided to re-build the world, which takes a while).

However, the error is still strange. Is there some undetected failure in an 
earlier cd command?