diff options
| author | David Aspinall | 1998-10-12 16:37:02 +0000 |
|---|---|---|
| committer | David Aspinall | 1998-10-12 16:37:02 +0000 |
| commit | ecb7fa25b913a4a17378344275f727b4ec90c3a6 (patch) | |
| tree | c50865f990a7b1d550653acd32ea0a00e5da270d | |
| parent | 49e285ec2732c322303cada3280855931924783c (diff) | |
Notes about things to put in docs.
| -rw-r--r-- | Makefile.devel | 2 | ||||
| -rw-r--r-- | doc/notes.txt | 8 |
2 files changed, 9 insertions, 1 deletions
diff --git a/Makefile.devel b/Makefile.devel index 652029c4..26581efa 100644 --- a/Makefile.devel +++ b/Makefile.devel @@ -56,7 +56,7 @@ EMACS=xemacs # Files not to include the distribution area or tarball -NONDISTFILES=todo html etc Makefile doc/Makefile images/*.xcf images/notes.txt images/gimp images/Makefile +NONDISTFILES=todo html etc Makefile doc/Makefile doc/notes.txt images/*.xcf images/notes.txt images/gimp images/Makefile # Files not to include in the distribution tarball IGNOREDFILES=doc/ProofGeneral.dvi diff --git a/doc/notes.txt b/doc/notes.txt new file mode 100644 index 00000000..9edd6529 --- /dev/null +++ b/doc/notes.txt @@ -0,0 +1,8 @@ +Notes to include in documentation. +---------------------------------- + + +Why is C-c C-b useful? Could just use the file to read it one go +(will we have a command to do this other than via the process?). +BUT it's nice because it stops exactly where a proof fails, so you can +continue development from there. |