--- a/Admin/website/dist/index.html Sat Jun 04 21:35:20 2005 +0200
+++ b/Admin/website/dist/index.html Sat Jun 04 21:35:20 2005 +0200
@@ -1,6 +1,6 @@
<?xml version='1.0' encoding='iso-8859-1' ?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
-<?cvs id="$Id$"?>
+<!-- $Id$ -->
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
@@ -19,15 +19,13 @@
<p>First, you might like to switch to a nearby mirror:</p>
<ul>
- <li><a href=
- "http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/download.html">Cambridge
+ <li><a href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/download.html">Cambridge
(UK)</a></li>
<li><a href="http://isabelle.in.tum.de/dist/download.html">Munich
(Germany)</a></li>
- <li><a href=
- "http://mirror.cse.unsw.edu.au/pub/isabelle/download.html">Sydney
+ <li><a href="http://mirror.cse.unsw.edu.au/pub/isabelle/download.html">Sydney
(Australia)</a></li>
</ul>
</div>