Caution: we set no default value, so the g5k configuration (in
g5k-platform-production) needs to be updated!