diff -r bb282845ca77 -r 173efad74891 lib/scripts/isa-xterm --- 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 }