New files.

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.