equal
deleted
inserted
replaced
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," |
16 echo " -o FORMAT specify output format: dvi (default), dvi.gz, ps, ps.gz," |
17 echo " pdf, or bbl" |
17 echo " pdf, or bbl" |
18 echo |
18 echo |
19 echo |
19 echo " Run LaTeX (and related tools) on FILE (default root.tex)," |
20 echo " Run LaTeX (and related tools) on FILE (default root.tex), producing the" |
20 echo " producing the specified output format." |
21 echo " speficied output format." |
|
22 echo |
21 echo |
23 exit 1 |
22 exit 1 |
24 } |
23 } |
25 |
24 |
26 function fail() |
25 function fail() |