diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2004-04-14 16:30:28 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2004-04-14 16:30:28 +0000 |
| commit | c621a2ea58e24b04db91787e38a6842fe80a477b (patch) | |
| tree | 85812d968446d7690ccc2986108a4d26283daea6 /pgshell | |
| parent | c230e600adeb35f4c174c68812712cf50a45fe44 (diff) | |
Updated.
Diffstat (limited to 'pgshell')
| -rw-r--r-- | pgshell/README | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/pgshell/README b/pgshell/README index ff6897e6..4dd96aa1 100644 --- a/pgshell/README +++ b/pgshell/README @@ -1,6 +1,9 @@ Proof General for shell scripts/simple command interpreters. -David Aspinall. +Author: David Aspinall +Status: Supported; experimental + +==================================================================== This instance of PG is handy just for using script management to cut-and-paste into a buffer running an ordinary shell of some kind. |