# HG changeset patch
# User wenzelm
# Date 1604848764 -3600
# Node ID feb80142e5721e82627b6be1fa2cf1b564cc55c2
# Parent  49057e93f56762e06b8b760ed9b0af655c606f5b
proper list_url, suitable for composition;

diff -r 49057e93f567 -r feb80142e572 src/Pure/General/mailman.scala
--- a/src/Pure/General/mailman.scala	Sun Nov 08 15:02:50 2020 +0100
+++ b/src/Pure/General/mailman.scala	Sun Nov 08 16:19:24 2020 +0100
@@ -20,9 +20,11 @@
     val hrefs = """href="([^"]+\.txt(?:\.gz)?)"""".r.findAllMatchIn(text).map(_.group(1)).toList
     val title =
       """<title>The ([^</>]*) Archives</title>""".r.findFirstMatchIn(text).map(_.group(1))
+    val list_url =
+      Url(Library.take_suffix[Char](_ == '/', Url.trim_index(url).toString.toList)._1.mkString + "/")
     val list_name =
       (proper_string(name) orElse title).getOrElse(error("Failed to determine mailing list name"))
-    new Archive(Url.trim_index(url), list_name, hrefs)
+    new Archive(list_url, list_name, hrefs)
   }
 
   class Archive private[Mailman](val list_url: URL, val list_name: String, hrefs: List[String])