diff options
Diffstat (limited to 'pgshell/README')
| -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. |