--- a/docs/build-docs.sh	Fri Sep 29 03:03:17 2006 +0000
+++ b/docs/build-docs.sh	Tue Oct 03 15:17:47 2006 +0000
@@ -21,8 +21,8 @@
 		$GIFTOPNM "$i" | $PNMTOPS -scale=0.5 -noturn > `echo "$i" | sed "s/.gif/.eps/"`
 	done
 else
-	echo "WARNING! No supported image conversion tools found, not converting images."
-	echo "This may cause some document format conversions to fail or produce errors."
+	echo "*** WARNING! No supported image conversion tools found, not converting images."
+	echo "*** This may cause some document format conversions to fail or produce errors."
 fi
 
 
@@ -30,7 +30,7 @@
 if test -n "$JW" && test -x "$JW"; then
 	echo "** DocBook SGML tools and JW found(?) Generating documentation ..."
 else
-	echo "ERROR! Jade Wrapper does not seem to be installed."
+	echo "*** ERROR! Jade Wrapper does not seem to be installed."
 	echo "You must have DocBook SGML tools/schemas and JadeTex installed"
 	echo "in order to generate the documentation."
 	exit 1
@@ -53,6 +53,8 @@
 	if test -n "$JW" && test -x "$JW"; then
 		echo "** Found, cleaning up the mess by DocBook .."
 		$TIDY -asxhtml -i -m $HTMLPATH/*.html
+	else
+		echo "*** WARNING! HTML tidy not found."
 	fi
 fi
 
@@ -70,8 +72,8 @@
 	$GS -dSAFER -dCompatibilityLevel=1.2 -q -dNOPAUSE -dBATCH -sDEVICE=pdfwrite \
 	-sOutputFile=manual.pdf -dCompatibilityLevel=1.2 -c .setpdfwrite -f manual.ps
 else
-	echo "WARNING! GhostScript does not seem to be installed."
-	echo "PDF version of the manual will not be generated."
+	echo "*** WARNING! GhostScript does not seem to be installed."
+	echo "*** PDF version of the manual will not be generated."
 fi
 
 ### Generate ASCII text