--- a/Admin/website/TODO Tue Jun 28 12:25:19 2005 +0200
+++ b/Admin/website/TODO Tue Jun 28 12:32:38 2005 +0200
@@ -4,6 +4,8 @@
the relationship between main and dist
--> add a "stripprefix" to directive
+- better argument handling in pypager
+
- centralize scattered project partners informations at "community"
- move projects from "overview" to "community"
--- a/Admin/website/build/pypager.py Tue Jun 28 12:25:19 2005 +0200
+++ b/Admin/website/build/pypager.py Tue Jun 28 12:32:38 2005 +0200
@@ -170,6 +170,8 @@
thisloc = self._pc.relLocOfThis()
if thisloc.startswith(stripprefix):
thisloc = thisloc[len(stripprefix):]
+ else:
+ raise Exception("Incompatible mirror (prefix to strip not found): %s" % title.encode("latin-1"))
handler.startElement(u"a", {u"href": posixpath.join(prefix, thisloc)})
handler.characters(title)
handler.endElement(u"a")
--- a/Admin/website/dist/documentation.html Tue Jun 28 12:25:19 2005 +0200
+++ b/Admin/website/dist/documentation.html Tue Jun 28 12:32:38 2005 +0200
@@ -15,7 +15,7 @@
<div class="hr"><hr/></div>
<div id="content">
-
+ <?include file="//include/mirrorlist.minor.include.html"?>
<h2>Getting started</h2>
<a href="//dist/img/tutorial_cover_big.gif">
--- a/Admin/website/dist/download.html Tue Jun 28 12:25:19 2005 +0200
+++ b/Admin/website/dist/download.html Tue Jun 28 12:32:38 2005 +0200
@@ -14,7 +14,7 @@
<?include file="//include/navigation_dist.include.html"?>
<div class="hr"><hr/></div>
<div id="content">
-
+ <?include file="//include/mirrorlist.minor.include.html"?>
<h2><?value key="distname"?></h2>
<p>The following source and binary packages of <?value key="distname"?>
--- a/Admin/website/overview.html Tue Jun 28 12:25:19 2005 +0200
+++ b/Admin/website/overview.html Tue Jun 28 12:32:38 2005 +0200
@@ -14,6 +14,7 @@
<?include file="//include/navigation.include.html"?>
<div class="hr"><hr/></div>
<div id="content">
+ <?include file="//include/mirrorlist.major.include.html"?>
<h2>What is Isabelle?</h2>
<p>
Isabelle is a generic proof assistant. It allows mathematical