c9cbce0fdb
this is to fix `make -j50' where `make -j18' worked. The race may just have been more likely to be lost for -j50.