more Mailman archives;
authorwenzelm
Fri, 10 Dec 2021 19:21:14 +0100
changeset 74907 af2323593473
parent 74906 9702913db56c
child 74908 7423bfe7c038
more Mailman archives;
src/Pure/Admin/isabelle_cronjob.scala
src/Pure/General/mailman.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)
       })
 
 
--- 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)
   }