| changeset 74907 | af2323593473 |
| parent 74906 | 9702913db56c |
| child 74921 | 74655fd58f8e |
--- 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) }