Only build extra docs if we have tetex installed #113023

--- docs/makefile
+++ docs/makefile
@@ -14,25 +14,25 @@
 all: usermanual.ps usermanual.pdf html/usermanual_1.html ucblogo.info
 
 ucblogo.info: usermanual.texi
-	makeinfo usermanual.texi
+	-makeinfo usermanual.texi
 
 usermanual.dvi: usermanual.texi
-	tex --interaction batchmode usermanual.texi
-	tex --interaction batchmode usermanual.texi
-	texindex usermanual.cp
-	tex --interaction batchmode usermanual.texi
+	-tex --interaction batchmode usermanual.texi
+	-tex --interaction batchmode usermanual.texi
+	-texindex usermanual.cp
+	-tex --interaction batchmode usermanual.texi
 
 usermanual.ps: usermanual.dvi
-	dvips -t letter -o usermanual.ps usermanual.dvi
+	-dvips -t letter -o usermanual.ps usermanual.dvi
 
 usermanual.pdf: usermanual.ps usermanual.dvi
-	ps2pdf usermanual.ps
-	dvipdf usermanual.dvi
+	-ps2pdf usermanual.ps
+	-dvipdf usermanual.dvi
 
 html/usermanual_1.html: usermanual.texi
 	for d in html; do [ -d $$d ] || mkdir -p $$d || exit 1; done
-	texi2html -expand tex -split chapter usermanual.texi
-	mv *.html html
+	-texi2html -expand tex -split chapter usermanual.texi
+	-mv *.html html
 
 ship:
 	-rm -f *.{aux,cp,cps,dvi,fn,ky,log,pg,toc,tp,vr}