# HG changeset patch
# User wenzelm
# Date 968770874 -7200
# Node ID aea053733eb0be734771252f9dce7ae74628ddd6
# Parent  9feb1e0c4cb3629aa698525b5e720d5db1a12542
tuned;

diff -r 9feb1e0c4cb3 -r aea053733eb0 Admin/makedist
--- a/Admin/makedist	Tue Sep 12 15:43:15 2000 +0200
+++ b/Admin/makedist	Tue Sep 12 17:01:14 2000 +0200
@@ -221,7 +221,7 @@
 mv "$DISTNAME" "${DISTNAME}-old"
 mkdir "$DISTNAME"
 
-mv "${DISTNAME}-old/README.html" "${DISTNAME}-old/INSTALL" "$DISTNAME"
+mv "${DISTNAME}-old/README.html" "${DISTNAME}-old/INSTALL" "${DISTNAME}-old/NEWS" "$DISTNAME"
 mkdir "$DISTNAME/doc"
 mv "${DISTNAME}-old/doc/"*.pdf "$DISTNAME/doc"
 
diff -r 9feb1e0c4cb3 -r aea053733eb0 Admin/page/dist-content/binary.content
--- a/Admin/page/dist-content/binary.content	Tue Sep 12 15:43:15 2000 +0200
+++ b/Admin/page/dist-content/binary.content	Tue Sep 12 17:01:14 2000 +0200
@@ -3,6 +3,14 @@
 
 %body%
 
+<p>
+
+The binary distribution is designed for easy installation of Isabelle
+and related tools (Proof General and X-Symbol) on common platforms.
+There is no manual intervention requires, no need to edit config files
+etc. by hand.
+
+
 <h2>(1) Linux/x86 systems with RPM</h2>
 
 This is the binary distribution of <!-- _GP_ distname --> for
diff -r 9feb1e0c4cb3 -r aea053733eb0 Admin/page/dist-content/docs.content
--- a/Admin/page/dist-content/docs.content	Tue Sep 12 15:43:15 2000 +0200
+++ b/Admin/page/dist-content/docs.content	Tue Sep 12 17:01:14 2000 +0200
@@ -6,5 +6,5 @@
 
 <!-- _GP_ include("$pwd/docu-contents.dist") -->
 
-All this documentation is also part of the Isabelle <a
-href="source.html">distribution</a> (both as dvi and pdf).
+All this documentation is also part of the Isabelle distribution (both
+as dvi and pdf).
diff -r 9feb1e0c4cb3 -r aea053733eb0 Admin/page/dist-content/source.content
--- a/Admin/page/dist-content/source.content	Tue Sep 12 15:43:15 2000 +0200
+++ b/Admin/page/dist-content/source.content	Tue Sep 12 17:01:14 2000 +0200
@@ -21,7 +21,8 @@
 
 Please see the Isabelle <!-- _GP_ href(distname . "/README.html",
 "README") --> and <!-- _GP_ href(distname . "/INSTALL", "INSTALL") -->
-files for more information.
+files for more information.  See the <!-- _GP_ href(distname
+. "/NEWS", "NEWS") --> file for a history user-relevant changes.
 
 <p>