Makefile.in
changeset 10239 cf55a4c21e7f
parent 10220 64461831f72d
child 10244 b0fd746c5532
--- a/Makefile.in	Tue Oct 14 19:27:08 2008 +0000
+++ b/Makefile.in	Tue Oct 14 19:47:28 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 "----------------"