46bed32fc6
after "."), remove some whitespace left over from when we removed Makefile.options. This commit was SVN r7393.