diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 1999-10-01 10:31:20 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 1999-10-01 10:31:20 +0000 |
| commit | ac70c9a82d5cc364c414c4e3d3299cf09d1d3670 (patch) | |
| tree | aef2dc2e7d899796827f50f79ff774ae7d770808 | |
| parent | 57f530aad7a13ddd08c61aa3a514732361b599f9 (diff) | |
No attempt to update BUGS section of manual
| -rw-r--r-- | doc/ProofGeneral.texi | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index 9b7ea2bb..f302e650 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -3885,10 +3885,11 @@ support for provers you don't use. @appendix Known bugs and workarounds We mention some of the known problems with Proof General here. The list -is not a description of all bugs and may be out of date. @* -Please consult the file +was written for Proof General 2.0. It is not a description of all bugs +and may be out of date. @* Please consult the file @uref{http://www.dcs.ed.ac.uk/home/proofgen/ProofGeneral/BUGS,@file{BUGS}} in the distribution for more detailed and up-to-date information. @* + If you discover a problem which isn't mentioned in @file{BUGS}, please let us know by sending a note to @code{proofgen@@dcs.ed.ac.uk}. @@ -3999,7 +4000,8 @@ If LEGO 1.3.1 attempts to write a (object) file in a non-writable directory, it forgets the protocol mechanism on how to interact with Proof General and gets stuck. -@strong{Workaround:} Directly enter @kbd{Configure AnnotateOn;} in the Proof Shell to recover. +@strong{Workaround:} Directly enter @kbd{Configure AnnotateOn;} in the +Proof Shell to recover. @node Bugs specific to Coq Proof General @section Bugs specific to Coq Proof General @@ -4013,7 +4015,7 @@ Thus, user-defined tactics cannot be retracted. @subsection Sections -The Coq Proof General does not know about Coq's section mechanism. +Coq Proof General does not know about Coq's Section mechanism. @c @c Isabelle Bugs |