diff options
Diffstat (limited to 'pgshell')
| -rw-r--r-- | pgshell/README | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/pgshell/README b/pgshell/README new file mode 100644 index 00000000..ff6897e6 --- /dev/null +++ b/pgshell/README @@ -0,0 +1,17 @@ +Proof General for shell scripts/simple command interpreters. + +David Aspinall. + +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. + +I'm providing this so that tool demonstrators may use it instead of +tediously doing cut-and-paste of commands from a file. No history +management, and nothing to do with theorem proving really! + +To use this instance of PG, visit a file with the ".pgsh" extension. + +You can modify the settings in pgshell.el to suit your application +(e.g. run some program other than the shell). + +Feedback welcome. |