Pilot error:
  rm -rf &
doesn't delete the build directory. With a really empty directory works.

Sorry for the noise!

(Besides, the correct patch would have been http://gcc.gnu.org/ml/gcc-patches/2013-10/msg00939.html )

Tobias

Reply via email to