changeset 8080 | 6927201dcff3 |
parent 7294 | b53e8aae866c |
child 8289 | 6eaeffc28704 |
--- a/configure Sat Dec 15 22:05:02 2007 +0000 +++ b/configure Sat Dec 15 22:42:12 2007 +0000 @@ -31,7 +31,7 @@ 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