configure
branchNewGRF_ports
changeset 6872 1c4a4a609f85
parent 6732 ca1b466db422
child 10211 c1391c8ed5c6
--- a/configure	Mon Dec 03 23:39:38 2007 +0000
+++ b/configure	Tue Jan 22 21:00:30 2008 +0000
@@ -31,13 +31,13 @@
 MEDIA_DIR="$ROOT_DIR/media"
 SOURCE_LIST="$ROOT_DIR/source.list"
 
-if [ "$1" = "--reconfig" ]; then
+if [ "$1" = "--reconfig" ] || [ "$1" = "--reconfigure" ]; then
 	if ! [ -f "config.cache" ]; then
 		echo "can't reconfigure, because never configured before"
 		exit 1
 	fi
 	# Make sure we don't lock config.cache
-	cat config.cache > cache.tmp
+	cat config.cache | sed 's/\\ /\\\\ /g' > cache.tmp
 	sh cache.tmp
 	rm -f cache.tmp
 	exit $?