echo "special publish started"
rm  *.log *.toc all.ps* all.dvi* pdf.pdf* >& /dev/null
gunzip KnowingUfoVisitors.eps.gz
gunzip LoewenheimSkolemHerbrand-FinalBridge.eps.gz
gunzip herbrand.eps.gz
latex pdf | egrep 'rorr|l\.[0-9]+ ' 
latex pdf | egrep 'rorr|l\.[0-9]+ ' 
latex pdf | egrep 'arning|rorr|l\.[0-9]+ ' 
makeindex pdf
latex pdf | egrep 'rorr|l\.[0-9]+ ' 
latex pdf | egrep 'rorr|l\.[0-9]+ ' 
latex pdf | egrep 'arning|rorr|l\.[0-9]+ ' 
makeindex pdf
latex pdf | egrep 'rorr|l\.[0-9]+ ' 
latex pdf | egrep 'rorr|l\.[0-9]+ ' 
latex pdf | egrep 'arning|rorr|l\.[0-9]+ ' 
makeindex pdf
mydvips pdf
# ps2pdf14 pdf.ps
ps2pdf14 -dPDFSETTINGS=/prepress -dEmbedAllFonts=true pdf.ps
rm pdf.ps
laall
laall
laall
makeindex all
laall
laall
laall
makeindex all
laall
laall
laall
laall
mydvips all
gzip -9 all.ps
gzip -9 all.dvi
chmod go+r all.ps.gz pdf.pdf all.dvi.gz welcome.html
gzip -9  *.eps &
rm  pdf.dvi *.log *.toc >& /dev/null
ls -al ~/WWW/p/herbrandSEKI
echo "special publish finished"
echo "Please do not rerun this command before its gzip jobs have terminated!"