changeset 7459 | 173efad74891 |
parent 7241 | 8f3c14d60345 |
child 8598 | f625793c4fff |
--- a/lib/scripts/isa-xterm Fri Sep 03 16:11:53 1999 +0200 +++ b/lib/scripts/isa-xterm Fri Sep 03 17:52:13 1999 +0200 @@ -25,6 +25,8 @@ echo " Starts Isabelle within an xterm window. CMDLINE is passed" echo " directly to the isabelle session." echo + echo " ISABELLE_XTERM_OPTIONS=$ISABELLE_XTERM_OPTIONS" + echo exit 1 }