config.lib
changeset 7347 7a77358b0537
parent 7346 3c376020c6bf
child 7414 54c0982e17ab
--- a/config.lib	Mon Jun 11 10:01:03 2007 +0000
+++ b/config.lib	Mon Jun 11 10:29:07 2007 +0000
@@ -531,6 +531,7 @@
 	if [ "$with_distcc" != "0" ]; then
 		res="`$distcc --version 2>/dev/null | head -n 1 | cut -b 0-6`"
 		if [ "$res" != "distcc" ]; then
+			distcc=""
 			log 1 "checking distcc... no"
 			if [ "$with_distcc" = "2" ]; then
 				log 1 "configure: error: no distcc detected, but was forced to be used"
@@ -1935,6 +1936,7 @@
 		s#!!AWK!!#$awk#g;
 		s#!!GCC295!!#$gcc295#g;
 		s#!!ENABLE_INSTALL!!#$enable_install#g;
+		s#!!DISTCC!!#$distcc#g;
 	"
 }