src/Pure/Tools/build_docker.scala
Wed, 06 Mar 2019 21:44:30 +0100 wenzelm proper option (amending cc0b3e177b49);
Mon, 06 Aug 2018 15:43:36 +0200 wenzelm updated for release;
Mon, 23 Oct 2017 19:30:39 +0200 wenzelm updated to jdk-8u152, which is for x86_64 only;
Sun, 08 Oct 2017 14:52:06 +0200 wenzelm build_docker is regular tool (non-admin);
less more (0) tip