lib/scripts/isa-xterm
changeset 7459 173efad74891
parent 7241 8f3c14d60345
child 8598 f625793c4fff
equal deleted inserted replaced
7458:bb282845ca77 7459:173efad74891
    22   echo "    -s BOOL      symbolic font output? (default true)"
    22   echo "    -s BOOL      symbolic font output? (default true)"
    23   echo "    -x PRG       executable program (default xterm)"
    23   echo "    -x PRG       executable program (default xterm)"
    24   echo
    24   echo
    25   echo "  Starts Isabelle within an xterm window. CMDLINE is passed"
    25   echo "  Starts Isabelle within an xterm window. CMDLINE is passed"
    26   echo "  directly to the isabelle session."
    26   echo "  directly to the isabelle session."
       
    27   echo
       
    28   echo "  ISABELLE_XTERM_OPTIONS=$ISABELLE_XTERM_OPTIONS"
    27   echo
    29   echo
    28   exit 1
    30   exit 1
    29 }
    31 }
    30 
    32 
    31 function fail()
    33 function fail()