cd doc
stack 50000

echo "	tex TritonDev.texi"
tex TritonDev.texi
echo "	texindex TritonDev.cp"
texindex TritonDev.cp
echo "	tex TritonDev.texi"
tex TritonDev.texi