equal
deleted
inserted
replaced
13 echo "Usage: $PRG [OPTIONS] [DIR]" |
13 echo "Usage: $PRG [OPTIONS] [DIR]" |
14 echo |
14 echo |
15 echo " Options are:" |
15 echo " Options are:" |
16 echo " -o FORMAT specify output format: dvi (default), dvi.gz, ps, ps.gz, pdf" |
16 echo " -o FORMAT specify output format: dvi (default), dvi.gz, ps, ps.gz, pdf" |
17 echo |
17 echo |
18 echo |
18 echo " Prepare the theory session document in DIR (default '.')" |
19 echo " Prepare the theory session document in DIR (default .)" |
19 echo " producing the specified output format." |
20 echo " producing the speficied output format." |
|
21 echo |
20 echo |
22 exit 1 |
21 exit 1 |
23 } |
22 } |
24 |
23 |
25 function fail() |
24 function fail() |