# HG changeset patch
# User wenzelm
# Date 1639160474 -3600
# Node ID af2323593473df93fd941b01bcca6aae1c1d1295
# Parent  9702913db56c636f74de513e5e5e9a127e755d96
more Mailman archives;

diff -r 9702913db56c -r af2323593473 src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Fri Dec 10 18:56:18 2021 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Fri Dec 10 19:21:14 2021 +0100
@@ -75,8 +75,8 @@
   val mailman_archives: Logger_Task =
     Logger_Task("mailman_archives", logger =>
       {
-        Mailman.isabelle_users.download_text(mailman_archives_dir)
-        Mailman.isabelle_dev.download_text(mailman_archives_dir)
+        Mailman.isabelle_users.download(mailman_archives_dir)
+        Mailman.isabelle_dev.download(mailman_archives_dir)
       })
 
 
diff -r 9702913db56c -r af2323593473 src/Pure/General/mailman.scala
--- a/src/Pure/General/mailman.scala	Fri Dec 10 18:56:18 2021 +0100
+++ b/src/Pure/General/mailman.scala	Fri Dec 10 19:21:14 2021 +0100
@@ -81,6 +81,10 @@
 
     def download_msg(target_dir: Path, progress: Progress = new Progress): List[Path] =
       hrefs_msg.flatMap(get(target_dir, _, progress = progress))
+
+    def download(target_dir: Path, progress: Progress = new Progress): List[Path] =
+      download_text(target_dir, progress = progress) :::
+      download_msg(target_dir, progress = progress)
   }