diff options
author | Norbert Preining <norbert@preining.info> | 2019-09-02 13:46:59 +0900 |
---|---|---|
committer | Norbert Preining <norbert@preining.info> | 2019-09-02 13:46:59 +0900 |
commit | e0c6872cf40896c7be36b11dcc744620f10adf1d (patch) | |
tree | 60335e10d2f4354b0674ec22d7b53f0f8abee672 /support/proof/edit |
Initial commit
Diffstat (limited to 'support/proof/edit')
-rwxr-xr-x | support/proof/edit | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/support/proof/edit b/support/proof/edit new file mode 100755 index 0000000000..bb3f03c6c5 --- /dev/null +++ b/support/proof/edit @@ -0,0 +1,22 @@ +#!/bin/bash + +# $Id: edit,v 1.2 2002/09/30$ + +# +# Sample editing script (Usage: edit sourcefile) +# + +editor=${EDITOR:-vi} # <-- Enter your favourite editor here! +XOFF=0 # <-- Enter Proof's x-term window x offset here! +YOFF=0 # <-- Enter Proof's x-term window y offset here! + +[ $TERM != 'xterm' ] && { echo 'No graphical user interface!'; exit 1; } + +xterm -geometry "80x15+$XOFF+$YOFF" \ + -title 'Proof' \ + -e proof -P $1 & + +$editor $1 + +proof -T $1 + |