lib/scripts/isa-xterm
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
 }