diff -r a1f8d7d4084b -r b07ed0c2f89f Admin/page/main-content/index.content
--- a/Admin/page/main-content/index.content	Thu Sep 28 23:00:11 2000 +0200
+++ b/Admin/page/main-content/index.content	Thu Sep 28 23:00:55 2000 +0200
@@ -35,11 +35,6 @@
 
 <h2>Obtaining Isabelle</h2>
 
-You get <strong><!-- _GP_ distname --></strong> in the 
-<a href="dist/index.html">distribution area</a>.
-
-<p>
-
 The <strong><!-- _GP_ distname --></strong> distribution is available
 from several <a href="dist/index.html">mirror sites</a>.  It includes
 source and binary packages and browsable documentation.