lib/Tools/display
changeset 28650 a7ba12e0d3b7
parent 21342 223a3de1222b
child 29143 72c960b2b83e
equal deleted inserted replaced
28649:58ab885469f5 28650:a7ba12e0d3b7
     9 PRG="$(basename "$0")"
     9 PRG="$(basename "$0")"
    10 
    10 
    11 function usage()
    11 function usage()
    12 {
    12 {
    13   echo
    13   echo
    14   echo "Usage: $PRG [OPTIONS] FILE"
    14   echo "Usage: isabelle $PRG [OPTIONS] FILE"
    15   echo
    15   echo
    16   echo "  Options are:"
    16   echo "  Options are:"
    17   echo "    -c           cleanup -- remove FILE after use"
    17   echo "    -c           cleanup -- remove FILE after use"
    18   echo
    18   echo
    19   echo "  Display document FILE (in DVI or PDF format)."
    19   echo "  Display document FILE (in DVI or PDF format)."