diff options
Diffstat (limited to 'pgshell/example.pgsh')
-rw-r--r-- | pgshell/example.pgsh | 34 |
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. +# + + + + + + |