src/Pure/Tools/build_docker.scala
23 months ago wenzelm 2017-10-08 build_docker is regular tool (non-admin);