lib/Tools/latex
changeset 7857 a49a3978fe3a
parent 7815 cd0fe98db185
child 7865 d9be8bc5624e
equal deleted inserted replaced
7856:7d06972db6ca 7857:a49a3978fe3a
    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()