equal
deleted
inserted
replaced
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] [DIR]" |
14 echo "Usage: isabelle $PRG [OPTIONS] [DIR]" |
15 echo |
15 echo |
16 echo " Options are:" |
16 echo " Options are:" |
17 echo " -c cleanup -- be aggressive in removing old stuff" |
17 echo " -c cleanup -- be aggressive in removing old stuff" |
18 echo " -n NAME specify document name (default 'document')" |
18 echo " -n NAME specify document name (default 'document')" |
19 echo " -o FORMAT specify output format: dvi (default), dvi.gz, ps, ps.gz, pdf" |
19 echo " -o FORMAT specify output format: dvi (default), dvi.gz, ps, ps.gz, pdf" |