--- a/Admin/website/build/pypager.py Tue Jun 28 12:16:01 2005 +0200
+++ b/Admin/website/build/pypager.py Tue Jun 28 12:25:19 2005 +0200
@@ -166,7 +166,11 @@
prefix = args[u"prefix"]
title = args[u"title"]
- handler.startElement(u"a", {u"href": posixpath.join(prefix, self._pc.relLocOfThis())})
+ stripprefix = args.get(u"stripprefix", u"")
+ thisloc = self._pc.relLocOfThis()
+ if thisloc.startswith(stripprefix):
+ thisloc = thisloc[len(stripprefix):]
+ handler.startElement(u"a", {u"href": posixpath.join(prefix, thisloc)})
handler.characters(title)
handler.endElement(u"a")
--- a/Admin/website/include/mirrorlist.minor.include.html Tue Jun 28 12:16:01 2005 +0200
+++ b/Admin/website/include/mirrorlist.minor.include.html Tue Jun 28 12:25:19 2005 +0200
@@ -4,8 +4,8 @@
<div class="mirrorlist">
<p>Switch mirror:</p>
<ul>
- <li><?mirror prefix="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/" title="Cambridge (.uk)" ?></li>
- <li><?mirror prefix="http://isabelle.in.tum.de/" title="Munich (.de)" ?></li>
- <li><?mirror prefix="http://mirror.cse.unsw.edu.au/pub/isabelle/" title="Sydney (.au)" ?></li>
+ <li><?mirror prefix="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/" title="Cambridge (.uk)" ?></li>
+ <li><?mirror prefix="http://isabelle.in.tum.de/" title="Munich (.de)" ?></li>
+ <li><?mirror prefix="http://mirror.cse.unsw.edu.au/pub/isabelle/" title="Sydney (.au)" stripprefix="dist" ?></li>
</ul>
</div>