[FFmpeg-devel] [PATCH] configure: Detect old git domain and optionally update to it

[Reimar Döffinger]

On 2 Sep 2012, at 03:46, Michael Niedermayer <michaelni at gmx.at> wrote:
> Signed-off-by: Michael Niedermayer <michaelni at gmx.at>
> ---
> configure |   18 ++++++++++++++++++
> 1 file changed, 18 insertions(+)
> 
> diff --git a/configure b/configure
> index 3abe231..ca461e1 100755
> --- a/configure
> +++ b/configure
> @@ -2119,6 +2119,24 @@ else
>         die "Out of tree builds are impossible with config.h in source dir."
> fi
> 
> +if test -f "$source_path/.git/config" &&
> +   git remote -v | grep -i 'origin.*git at git.videolan.org:ffmpeg' > /dev/null ; then
> +    echolog "Outdated domain in git config, the official domain for ffmpeg git is since
> +November 2011, source.ffmpeg.org, both the old and the new point to the same
> +repository and server. To update to it press enter or CTRL-C to abort"
> +    read tmp
> +    git remote set-url origin git at source.ffmpeg.org:ffmpeg
> +fi
> +
> +if test -f "$source_path/.git/config" &&
> +   git remote -v | grep -i 'origin.*git://git.videolan.org/ffmpeg' > /dev/null ; then
> +    echolog "Outdated domain in git config, the official domain for ffmpeg git is since
> +November 2011, source.ffmpeg.org, both the old and the new point to the same
> +repository and server. To update to it press enter or CTRL-C to abort"
> +    read tmp
> +    git remote set-url origin git://source.ffmpeg.org/ffmpeg
> +fi

Since the wrong domain doesn't break anything yet I'd prefer if it just gave the command to change it, without blocking or changing it on its own.