# HG changeset patch
# User wenzelm
# Date 1662815897 -7200
# Node ID fbef5a48723f496eff87e170b5bd01b64358bc53
# Parent  f51e9da996a33f17e3aa5c74bcb95d3e1565bbac
more operations: for testing purposes;

diff -r f51e9da996a3 -r fbef5a48723f src/Pure/Tools/build_docker.scala
--- 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,