# HG changeset patch
# User wenzelm
# Date 1485207477 -3600
# Node ID 730bc1bcf27cccc929a121a67089cba483cb5d71
# Parent  19ca3644ec466f30bd3feb90d0914076c357a008
tuned;

diff -r 19ca3644ec46 -r 730bc1bcf27c src/Pure/Admin/build_docker.scala
--- a/src/Pure/Admin/build_docker.scala	Sun Jan 22 21:39:16 2017 +0100
+++ b/src/Pure/Admin/build_docker.scala	Mon Jan 23 22:37:57 2017 +0100
@@ -44,7 +44,7 @@
 
 # packages
 RUN apt-get -y update && \
-  apt-get install -y """ + (packages ::: more_packages).map(Bash.string(_)).mkString(" ") + """ && \
+  apt-get install -y """ + Bash.strings(packages ::: more_packages) + """ && \
   apt-get clean
 
 # user