Makefile.in
changeset 10220 64461831f72d
parent 10076 bdf576e96502
child 10239 cf55a4c21e7f
--- a/Makefile.in	Sun Oct 05 18:42:59 2008 +0000
+++ b/Makefile.in	Mon Oct 06 17:05:44 2008 +0000
@@ -91,7 +91,7 @@
 	@echo " Going to reconfigure with last known settings..."
 	@echo "----------------"
 # Make sure we don't lock config.cache
-	@$(shell cat config.cache | sed 's/\\ /\\\\ /g') || exit 1
+	@$(shell cat config.cache | sed 's#\\ #\\\\ #g') || exit 1
 	@echo "----------------"
 	@echo "Reconfig done. Please re-execute make."
 	@echo "----------------"