Links to developers todo files and README added. Prerelversion notified.

2 files changed, 34 insertions, 7 deletions

diff --git a/html/devel.phtml b/html/devel.phtml
index a55238d0..7a85b557 100644
--- a/html/devel.phtml
+++ b/html/devel.phtml
@@ -7,7 +7,11 @@ users and hackers!
 
 <ul>
 <li>
-Download the latest <a href="develdownload.phtml">development release</a>
+Download the latest <a href="develdownload.phtml">development release: 
+<!-- WARNING!  Line below automatically edited by makefile. -->
+ <b>ProofGeneral-3.1pre000301</b></a>
+<!-- end WARNING -->
+ <br>
  (please <a href="register.phtml">register</a> if you haven't already).
 </li>
 </ul>
@@ -24,6 +28,28 @@ Take a look at the Proof General <a href="projects.phtml">project proposals</a>.
 </ul>
 <ul>
 <li>
+Read the 
+developer's 
+<?php fileshow("ProofGeneral-3.1pre000301/README.devel","README file"); ?>, 
+with development hints and tips.
+</li>
+</ul>
+<ul>
+<li>
+See our current low-level lists of things to do, for the
+<!-- WARNING!  Lines below automatically edited by makefile. -->
+   <?php fileshow("ProofGeneral-3.1pre000301/todo","generic base"); ?>, 
+  <br>
+  and for each prover:
+   <?php fileshow("ProofGeneral-3.1pre000301/isa/todo","isa to do"); ?>,
+   <?php fileshow("ProofGeneral-3.1pre000301/isar/todo","isar to do"); ?>,
+   <?php fileshow("ProofGeneral-3.1pre000301/coq/todo","coq to do"); ?>,
+   <?php fileshow("ProofGeneral-3.1pre000301/lego/todo","lego to do"); ?>.
+<!-- end WARNING -->
+</li>
+</ul>
+<ul>
+<li>
 <?php hlink("feedback.phtml","Send us a message ","Feedback form")?>
 about any development issues.
 </li>
diff --git a/html/develdownload.phtml b/html/develdownload.phtml
index d79b9b58..52f9dd16 100644
--- a/html/develdownload.phtml
+++ b/html/develdownload.phtml
@@ -69,7 +69,12 @@ The complete archive also includes:
   </li>
   <li> the 
    <!-- WARNING!  Line below automatically edited by makefile. -->
-   <?php fileshow("ProofGeneral-3.1pre000301/todo","low-level list of things to do"); ?>
+   <?php fileshow("ProofGeneral-3.1pre000301/todo","generic low-level list of things to do"); ?>
+   and for each prover:
+   <?php fileshow("ProofGeneral-3.1pre000301/isa/todo","isa to do"); ?>,
+   <?php fileshow("ProofGeneral-3.1pre000301/isar/todo","isar to do"); ?>,
+   <?php fileshow("ProofGeneral-3.1pre000301/coq/todo","coq to do"); ?>,
+   <?php fileshow("ProofGeneral-3.1pre000301/lego/todo","lego to do"); ?>.
    <!-- End Warning. -->
    and the detailed
    <!-- WARNING!  Line below automatically edited by makefile. -->
@@ -89,11 +94,7 @@ release, because developers should have the right tools!
 <p>
 You probably <em>don't</em> need to download this if you're only
 interested in hacking the Emacs lisp part of the program for
-a prover that is currently supported.  But you may
-still like to check the latest
-<!-- WARNING!  Line below automatically edited by makefile. -->
-<?php fileshow("ProofGeneral-3.1pre000301/todo","low-level to-do list"); ?>.
-<!-- End Warning. -->
+a prover that is currently supported.  
 </p>
 
 <?php