cd doc
stack 50000

echo "	tex Triton.texi"
tex Triton.texi
echo "	texindex Triton.cp"
texindex Triton.cp
echo "	tex Triton.texi"
tex Triton.texi