From f1332103731a3a88fa8d91952d45b27dd0a333b7 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Tue, 13 Apr 2004 12:54:34 +0000 Subject: New files. --- pgshell/README | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) create mode 100644 pgshell/README (limited to 'pgshell') 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. -- cgit v1.2.3