+ echo "ERROR: *** $$tool is missing on your system."; \
+ echo " *** Because of this, I cannot compile $$toolsrc."; \
+ echo " *** If $$tool is installed but was not detected by configure,";\
+ echo " *** consider setting $$toolvar and re-running configure."; \
+ echo " *** See config.log for more details."; } >&2; false
+
+DEV_TOOL_ERROR = { \