[bcook]

If someone modifies GPL source-code and published the executable, they must publish the additional source-code.

Your quoted section only speaks of unmodified machine-code created from GPLed source-code.