tuned;
authorwenzelm
Mon, 23 Jan 2017 22:37:57 +0100
changeset 64941 730bc1bcf27c
parent 64940 19ca3644ec46
child 64942 bae35a568b1b
tuned;
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