diff -r 56b52fc25c95 -r d8ccbd5305bf src/Pure/build-jars --- a/src/Pure/build-jars Sat Jan 14 20:22:15 2017 +0100 +++ b/src/Pure/build-jars Sat Jan 14 20:33:55 2017 +0100 @@ -10,6 +10,7 @@ declare -a SOURCES=( Admin/build_doc.scala + Admin/build_docker.scala Admin/build_history.scala Admin/build_log.scala Admin/build_polyml.scala