src/Pure/Tools/build_docker.scala
Sun, 08 Oct 2017 14:52:06 +0200 wenzelm build_docker is regular tool (non-admin);
less more (0) tip