# HG changeset patch
# User wenzelm
# Date 1484426903 -3600
# Node ID 07a93485d22b360d2fca62ff0da2947f3791f2e6
# Parent  662de910a96bd4674cedca5073d4a0985ce20a2e
more options;

diff -r 662de910a96b -r 07a93485d22b src/Pure/Admin/build_docker.scala
--- a/src/Pure/Admin/build_docker.scala	Sat Jan 14 21:29:21 2017 +0100
+++ b/src/Pure/Admin/build_docker.scala	Sat Jan 14 21:48:23 2017 +0100
@@ -15,6 +15,7 @@
     app_archive: Path,
     logic: String = default_logic,
     output: Option[Path] = None,
+    packages: List[String] = Nil,
     tag: String = "",
     verbose: Boolean = false)
   {
@@ -35,7 +36,8 @@
 
 # packages
 RUN apt-get -y update && \
-  apt-get install -y less lib32stdc++6 libwww-perl rlwrap unzip && \
+  apt-get install -y less lib32stdc++6 libwww-perl rlwrap unzip """ +
+    packages.map(Bash.string(_)).mkString(" ") + """ && \
   apt-get clean
 
 # user
@@ -77,6 +79,7 @@
     {
       var logic = default_logic
       var output: Option[Path] = None
+      var packages: List[String] = Nil
       var verbose = false
       var tag = ""
 
@@ -87,6 +90,7 @@
   Options are:
     -l NAME      default logic (default ISABELLE_LOGIC=""" + quote(default_logic) + """)
     -o FILE      output generated Dockerfile
+    -p PACKAGE   additional Ubuntu package
     -t TAG       docker build tag
     -v           verbose
 
@@ -97,6 +101,7 @@
 """,
           "l:" -> (arg => logic = arg),
           "o:" -> (arg => output = Some(Path.explode(arg))),
+          "p:" -> (arg => packages ::= arg),
           "t:" -> (arg => tag = arg),
           "v" -> (_ => verbose = true))
 
@@ -107,6 +112,7 @@
           case _ => getopts.usage()
         }
 
-      build_docker(new Console_Progress(), app_archive, logic, output, tag, verbose)
+      build_docker(new Console_Progress(), app_archive, logic = logic, output = output,
+        packages = packages, tag = tag, verbose = verbose)
     }, admin = true)
 }