aboutsummaryrefslogtreecommitdiffhomepage
path: root/pgshell/example.pgsh
diff options
context:
space:
mode:
Diffstat (limited to 'pgshell/example.pgsh')
-rw-r--r--pgshell/example.pgsh34
1 files changed, 34 insertions, 0 deletions
diff --git a/pgshell/example.pgsh b/pgshell/example.pgsh
new file mode 100644
index 00000000..d7f860e5
--- /dev/null
+++ b/pgshell/example.pgsh
@@ -0,0 +1,34 @@
+# This is an example shell script for processing
+# with the script management of Proof General.
+#
+# It demonstrates the usefulness of PG simply for
+# sending a pre-defined sequence of commands to
+# some command-line interpreter, here /bin/sh.
+#
+# To adjust this for your needs, edit pgshell.el
+# (or copy and rename it).
+#
+# $Id$
+#
+
+# What time is it?
+date;
+
+# What machine am I on?
+uname -a;
+
+# What files are here?
+ls
+ -lt;
+
+# Notes:
+#
+# * Commands have to be terminated by ';'. Alternative is to write
+# your own scanner to recognize the start of the next command.
+#
+
+
+
+
+
+