# HG changeset patch
# User haftmann
# Date 1119954758 -7200
# Node ID 991ecdd985d932530896d7882c46655c12443606
# Parent  f2660fa6322451c5cfdb48433acfa7af76082ae7
introduced a notion of mirrors

diff -r f2660fa63224 -r 991ecdd985d9 Admin/website/TODO
--- 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"
diff -r f2660fa63224 -r 991ecdd985d9 Admin/website/build/pypager.py
--- 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")
diff -r f2660fa63224 -r 991ecdd985d9 Admin/website/dist/documentation.html
--- 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">
diff -r f2660fa63224 -r 991ecdd985d9 Admin/website/dist/download.html
--- 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"?>
diff -r f2660fa63224 -r 991ecdd985d9 Admin/website/overview.html
--- 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