Merge pull request #3778 from MartinNowak/fix13117

fix Issue 13117 - Executable size of hello world explodes from 472K to 2.7M