I think every advance that closes the gap between the Docker images being updated and the PRs is much welcome.
One of the reasons it is not live as it would seem logical to be, is because of security reasons (based on a chat long ago with @tqchen). We can’t blindly run a docker rebuild for any PR, because that opens the door for random people to run arbitrary commands on our Jenkins nodes, just by submitting a PR with changes to our shell scripts e.g. build.sh or bash.sh, which would run outside a container.
Does the proposed change here address this fundamental issue of the way our CI is organised?