This reverts commit 00b756f0e2. Unfortunately, I made a typo in the script and the fix did not work. I do not want to rebase the master (in order not to break things for everyone) so I am reverting again. Sorry.
00b756f0e2