Merge branch 'fix-buildserver' into 'master'

Merge branch 'fix-buildserver' into 'master'

Fix buildserver, broken by e449d2f

Switching to a script /etc/profile.d to set up the environment is all
well and good, except that doesn't get run when you directly execute a
command directly via ssh, which means that the buildserver didn't work
at all (at least for anything that used gradle, or relied on the
environment variables.

This fix doesn't look very nice, but it works - it just forces the
appropriate script to run before build.py is executed on the server.

(Side note, I thought we had tests for this, how did it get past them?)

See merge request !135