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)
   }