diff options
| author | David Aspinall | 2004-03-01 11:28:39 +0000 |
|---|---|---|
| committer | David Aspinall | 2004-03-01 11:28:39 +0000 |
| commit | c68de842dd9898d4a028f5a1e71c95cf3b95a02d (patch) | |
| tree | 6aa4c044872605df38bb0b850bab3d9aeec9e727 | |
| parent | cc5d0913b644a9d269773c96462f7563a9a1ae03 (diff) | |
Pass unrecognized options to Emacs
| -rw-r--r-- | bin/proofgeneral | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/bin/proofgeneral b/bin/proofgeneral index edbbe206..6def97ff 100644 --- a/bin/proofgeneral +++ b/bin/proofgeneral @@ -34,6 +34,8 @@ Options: -h, --help show this help and exit -v, --version output version information and exit +Unrecognized options are passed to Emacs, along with file names. + Examples: $NAME Example.thy Load Proof General editing Isar file Example.thy $NAME example.v Load Proof General editing Coq file Example.v @@ -73,9 +75,6 @@ while --emacsbin) EMACS=$2 shift;; - -*) - echo "$NAME: option $1 not recognized. Use $NAME --help for help." 1>&2 - exit 1;; *) break;; esac do shift; done |