author | wenzelm |
Sat, 10 Sep 2022 15:18:17 +0200 | |
changeset 76103 | fbef5a48723f |
parent 76102 | f51e9da996a3 |
child 76104 | 5ee70e689eb3 |
--- a/src/Pure/Tools/build_docker.scala Sat Sep 10 14:25:53 2022 +0200 +++ b/src/Pure/Tools/build_docker.scala Sat Sep 10 15:18:17 2022 +0200 @@ -21,6 +21,9 @@ "latex" -> List("texlive-fonts-extra", "texlive-font-utils", "texlive-latex-extra", "texlive-science")) + def all_packages: List[String] = + packages ::: package_collections.valuesIterator.flatten.toList + def build_docker(progress: Progress, app_archive: String, base: String = default_base,