+DEV_TOOL_ERROR = { \
+ echo "ERROR: *** $$tool is missing on your system."; \
+ echo " *** Because of this, I cannot compile $$toolsrc, but"; \
+ echo " *** (perhaps because you modified it) the sources appear out"; \
+ echo " *** of date. If $$tool is installed but was not detected by"; \
+ echo " *** configure, consired setting $$toolvar and re-running configure."; \
+ echo " *** See config.log for more details."; } >&2; false