Adding push configuration to .git/config

Adding push configuration to .git/config

[Nico -telmich- Schottelius]

[-- Attachment #1: Type: text/plain, Size: 857 bytes --]

Hello guys!

We are working pretty much with branches here and I think it would be
pretty cool, to make git-push recognize some configuratio in
~/.git/config that describes where to push what:

   git-push origin master:<name of worker> is what we currenty do
   manually

Nice would be

[branch "master"]
   remote-push          = origin
   remote-push-merge    = another_branch

And thus perhaps also changing the existing specs:

   remote = ... to remote-fetch = ...
   merge = ... to remote-fetch-merge = 

And perhaps it would also make sense to replace "refs/heads/master" with
only "master"?

What do you think about those three ideas?

Nico

-- 
Think about Free and Open Source Software (FOSS).
http://nico.schottelius.org/documentations/foss/the-term-foss/

PGP: BFE4 C736 ABE5 406F 8F42  F7CF B8BE F92A 9885 188C

[-- Attachment #2: Digital signature --]
[-- Type: application/pgp-signature, Size: 189 bytes --]

Re: Adding push configuration to .git/config

[Steffen Prohaska]

On Nov 21, 2007, at 11:55 AM, Nico -telmich- Schottelius wrote:

> Hello guys!
>
> We are working pretty much with branches here and I think it would be
> pretty cool, to make git-push recognize some configuratio in
> ~/.git/config that describes where to push what:
>
>    git-push origin master:<name of worker> is what we currenty do
>    manually
>
> Nice would be
>
> [branch "master"]
>    remote-push          = origin
>    remote-push-merge    = another_branch

This was discussed in a similar form here:

http://marc.info/?l=git&m=119384331712996&w=2
http://marc.info/?l=git&m=119400354601328&w=2

So, yes, I think it would be very useful.  I did not yet find
time to implement it.


> And thus perhaps also changing the existing specs:
>
>    remote = ... to remote-fetch = ...
>    merge = ... to remote-fetch-merge =

This is a logical consequence.  It gives more freedom to pull
from one repo and push to another one.

I'm not fully convinced, though, of the configuration names
you propose.  However, I have no better suggestion right away.


> And perhaps it would also make sense to replace "refs/heads/master"  
> with
> only "master"?

No.  We use full refnames everywhere.  I think we should stick
with them.

	Steffen

Re: Adding push configuration to .git/config

[Junio C Hamano]

Nico -telmich- Schottelius <nico-linux-git@schottelius.org>
writes:

> Nice would be
>
> [branch "master"]
>    remote-push          = origin
>    remote-push-merge    = another_branch
>
> And thus perhaps also changing the existing specs:
>
>    remote = ... to remote-fetch = ...
>    merge = ... to remote-fetch-merge = 

I do not think doing this is worth it, not because I think a
single branch.$name.remote should be good enough for everybody,
but because once you need a separate remote each for fetching
and pushing, there is no reason to say one per direction is
enough.

An alternative could be to split [remote "name"] url into two
variants, fetch-url and push-url.  While fetching by default
from two places without telling from which one does not make any
sense, pushing by default to two different places is quite a
normal thing to do, and we already do support more than one url
entries in [remote "name"] section used for pushing.

If we were to do this, it might also make sense to rename the
word 'origin' we use for the default remote name to 'default' or
something.  People with shared repository workflow would fetch
from one repository and push back to the same repository, so the
distinction would not matter, but for others who need something
like you suggest, the default repository for fetching and
pushing are different, and while you may still consider where
you fetch from your 'origin', where you push into is not your
'origin' anymore.

Re: Adding push configuration to .git/config

[Steffen Prohaska]

On Nov 22, 2007, at 2:48 AM, Junio C Hamano wrote:

> Nico -telmich- Schottelius <nico-linux-git@schottelius.org>
> writes:
>
>> Nice would be
>>
>> [branch "master"]
>>    remote-push          = origin
>>    remote-push-merge    = another_branch
>>
>> And thus perhaps also changing the existing specs:
>>
>>    remote = ... to remote-fetch = ...
>>    merge = ... to remote-fetch-merge =
>
> I do not think doing this is worth it, not because I think a
> single branch.$name.remote should be good enough for everybody,
> but because once you need a separate remote each for fetching
> and pushing, there is no reason to say one per direction is
> enough.
>
> An alternative could be to split [remote "name"] url into two
> variants, fetch-url and push-url.  While fetching by default
> from two places without telling from which one does not make any
> sense, pushing by default to two different places is quite a
> normal thing to do, and we already do support more than one url
> entries in [remote "name"] section used for pushing.
>
> If we were to do this, it might also make sense to rename the
> word 'origin' we use for the default remote name to 'default' or
> something.  People with shared repository workflow would fetch
> from one repository and push back to the same repository, so the
> distinction would not matter, but for others who need something
> like you suggest, the default repository for fetching and
> pushing are different, and while you may still consider where
> you fetch from your 'origin', where you push into is not your
> 'origin' anymore.

I like this idea.

But in addition, we should have a branch.$name.push line that
can contain a remote head to push to.  This can be used to
manage push's default on a per-branch basis.  So, different
branches can have different default refspecs, even when they
refer to the same remote.

The default remote of "git push" is either origin, or it is
specified in the branch configuration.  The following rules
would then be used to find the refspecs to push.  The first
rule that matches wins:
1) Command line overrides (e.g. "--all", "--current").
2) Check if branch.$name.push entry is available.
    (Would we allow multiple entries?)
3) Check if remote.$remotename.push entries are available.
4) Use default rule, which pushes matching branches.

	Steffen

Re: Adding push configuration to .git/config

[Andreas Ericsson]

Steffen Prohaska wrote:
> 
> On Nov 22, 2007, at 2:48 AM, Junio C Hamano wrote:
> 
>> Nico -telmich- Schottelius <nico-linux-git@schottelius.org>
>> writes:
>>
>>> Nice would be
>>>
>>> [branch "master"]
>>>    remote-push          = origin
>>>    remote-push-merge    = another_branch
>>>
>>> And thus perhaps also changing the existing specs:
>>>
>>>    remote = ... to remote-fetch = ...
>>>    merge = ... to remote-fetch-merge =
>>
>> I do not think doing this is worth it, not because I think a
>> single branch.$name.remote should be good enough for everybody,
>> but because once you need a separate remote each for fetching
>> and pushing, there is no reason to say one per direction is
>> enough.
>>
>> An alternative could be to split [remote "name"] url into two
>> variants, fetch-url and push-url.  While fetching by default
>> from two places without telling from which one does not make any
>> sense, pushing by default to two different places is quite a
>> normal thing to do, and we already do support more than one url
>> entries in [remote "name"] section used for pushing.
>>
>> If we were to do this, it might also make sense to rename the
>> word 'origin' we use for the default remote name to 'default' or
>> something.  People with shared repository workflow would fetch
>> from one repository and push back to the same repository, so the
>> distinction would not matter, but for others who need something
>> like you suggest, the default repository for fetching and
>> pushing are different, and while you may still consider where
>> you fetch from your 'origin', where you push into is not your
>> 'origin' anymore.
> 
> I like this idea.
> 

I don't. It's troublesome enough to try to teach the finer points
of git to my co-workers without different defaults between versions.

So far we're getting around the problem by the relatively crude
expedient of forcing everyone to update to the latest stable from
master each time I say so. It works, but doesn't scale too well, and
since every major distro now ships git packages, it would be nice if
default-names at least settled down and were only changed with new
major releases (that is, from 1.x to 2.x).

On the other hand, I'm sure we'll cope whatever you decide.

-- 
Andreas Ericsson                   andreas.ericsson@op5.se
OP5 AB                             www.op5.se
Tel: +46 8-230225                  Fax: +46 8-230231

Re: Adding push configuration to .git/config

[Junio C Hamano]

Andreas Ericsson <ae@op5.se> writes:

> Steffen Prohaska wrote:
>>
>> On Nov 22, 2007, at 2:48 AM, Junio C Hamano wrote:
>> ...
>>> If we were to do this, it might also make sense to rename the
>>> word 'origin' we use for the default remote name to 'default' or
>>> something.  People with shared repository workflow would fetch
>>> from one repository and push back to the same repository, so the
>>> distinction would not matter, but for others who need something
>>> like you suggest, the default repository for fetching and
>>> pushing are different, and while you may still consider where
>>> you fetch from your 'origin', where you push into is not your
>>> 'origin' anymore.
>>
>> I like this idea.
>
> I don't. It's troublesome enough to try to teach the finer points
> of git to my co-workers without different defaults between versions.

I don't like the s/origin/default/ part either, which was the
reason I said "it might".  That would be what I would have done
if I were doing git from scratch right now.

Re: Adding push configuration to .git/config

[Junio C Hamano]

Steffen Prohaska <prohaska@zib.de> writes:

> On Nov 22, 2007, at 2:48 AM, Junio C Hamano wrote:
> ...
>> An alternative could be to split [remote "name"] url into two
>> variants, fetch-url and push-url.  While fetching by default
>> from two places without telling from which one does not make any
>> sense, pushing by default to two different places is quite a
>> normal thing to do, and we already do support more than one url
>> entries in [remote "name"] section used for pushing.
>>
>> If we were to do this, it might also make sense to rename the
>> word 'origin' we use for the default remote name to 'default' or
>> something.  People with shared repository workflow would fetch
>> from one repository and push back to the same repository, so the
>> distinction would not matter, but for others who need something
>> like you suggest, the default repository for fetching and
>> pushing are different, and while you may still consider where
>> you fetch from your 'origin', where you push into is not your
>> 'origin' anymore.
>
> I like this idea.
>
> But in addition, we should have a branch.$name.push line that
> can contain a remote head to push to.

Yes, but.

At that point, I think you would introduce a mismatch between
the traditional semantics of refspec and what you are trying to
do, unless you are careful.

The traditional semantics of refspecs-tied-to-remote is strongly
based on the assumption: "I will push to this remote when these
local branches are all ready to be pushed out, and they will all
go there together as an atomic update.  When I am _that_ ready
to push, it does not matter which local branch I am on.  The
branches that matter are all in good shape when I push."

You are making the behaviour of push dependent on which branch
you are on.  During such a push, it is safe to assume that the
current branch is ready to be pushed out, but other ones can be
very much un-ready.  The user needs a safety valve to prevent
other branches from being pushed out.  Otherwise the user would
not be adding branch.$name.push to begin with.

It would probably need to become a target ref or a list of <URL,
target ref>, not a list of general refspecs like the value for
remote.$there.push variable.  For example, you would want to say
"while on master, push it to repository A as refs/heads/master
and to repository B as refs/remotes/satellite/master", which
would be a typical arrangement if you are working on a satellite
machine, A is the shared central repository and B is mothership
to your satellite machine.  The specification would talk only
about the target ref (not just "'can contain' a remote head to
push to"), and the source ref would always be the current
branch.

I guess you could use general refspec on branch.$name.push and
implement the safety by requiring (1) only one refspec appears
for such a variable, and (2) the LHS of the refspec matches the
$name of the branch, in order to make the parsing easier and to
keep the syntax uniform.

Or maybe I am being overly cautious again not to introduce any
more unnecessary user confusion, and just should give them even
longer rope to hang themselves.  I dunno.

Re: Adding push configuration to .git/config

[Steffen Prohaska]

On Nov 22, 2007, at 9:23 AM, Junio C Hamano wrote:

> Steffen Prohaska <prohaska@zib.de> writes:
>
>> On Nov 22, 2007, at 2:48 AM, Junio C Hamano wrote:
>> ...
>>> An alternative could be to split [remote "name"] url into two
>>> variants, fetch-url and push-url.  While fetching by default
>>> from two places without telling from which one does not make any
>>> sense, pushing by default to two different places is quite a
>>> normal thing to do, and we already do support more than one url
>>> entries in [remote "name"] section used for pushing.
>>>
>>> If we were to do this, it might also make sense to rename the
>>> word 'origin' we use for the default remote name to 'default' or
>>> something.  People with shared repository workflow would fetch
>>> from one repository and push back to the same repository, so the
>>> distinction would not matter, but for others who need something
>>> like you suggest, the default repository for fetching and
>>> pushing are different, and while you may still consider where
>>> you fetch from your 'origin', where you push into is not your
>>> 'origin' anymore.
>>
>> I like this idea.
>>
>> But in addition, we should have a branch.$name.push line that
>> can contain a remote head to push to.
>
> Yes, but.
>
> At that point, I think you would introduce a mismatch between
> the traditional semantics of refspec and what you are trying to
> do, unless you are careful.
>
> The traditional semantics of refspecs-tied-to-remote is strongly
> based on the assumption: "I will push to this remote when these
> local branches are all ready to be pushed out, and they will all
> go there together as an atomic update.  When I am _that_ ready
> to push, it does not matter which local branch I am on.  The
> branches that matter are all in good shape when I push."
>
> You are making the behaviour of push dependent on which branch
> you are on.  During such a push, it is safe to assume that the
> current branch is ready to be pushed out, but other ones can be
> very much un-ready.  The user needs a safety valve to prevent
> other branches from being pushed out.  Otherwise the user would
> not be adding branch.$name.push to begin with.

This is not the only reason.  If I'm thinking of a workflow
based on a shared repo, I see two more reasons

The user wants to limit the push to the current branch
because different branches in the remote (shared) repo may
have advanced.  The user does not want to the see errors by
"git push" that complain about non-fast-forwards.  The safety
valve is needed to protect from changes in the remote repo
(not for changes in the local one).

The second use case is to have multiple local branches that
refer to the same (shared) remote branch.  If you want to push
the changes directly to the (shared) remote branch, you need to
"rename" the branch during the push.  But you want to push only
a single branch: the current branch you're on.  Hence you need
a per-branch configuration if you want "git push" to to the
work for you automatically.  It would be nice if "git branch"
could be asked to set up branch.$name.push to point to the
correct remote branch (similar to "--track").

With what I have in mind in the longterm you could do

	git checkout -b foo origin/master
         work work work
	git checkout -b bar origin/master
	work work work
	git checkout foo
	git pull   # or git fetch; git rebase
	git push
	git checkout bar
	git branch -d foo
         work work, ... and later push bar, too

Note, there are several other changes needed before this would
work:
- "git checkout" would have to set branch.$name.push.
- "-d" would needs to be accept deletion if all changes are on
   shared remote branch.


> It would probably need to become a target ref or a list of <URL,
> target ref>, not a list of general refspecs like the value for
> remote.$there.push variable.  For example, you would want to say
> "while on master, push it to repository A as refs/heads/master
> and to repository B as refs/remotes/satellite/master", which
> would be a typical arrangement if you are working on a satellite
> machine, A is the shared central repository and B is mothership
> to your satellite machine.  The specification would talk only
> about the target ref (not just "'can contain' a remote head to
> push to"), and the source ref would always be the current
> branch.
>
> I guess you could use general refspec on branch.$name.push and
> implement the safety by requiring (1) only one refspec appears
> for such a variable, and (2) the LHS of the refspec matches the
> $name of the branch, in order to make the parsing easier and to
> keep the syntax uniform.
>
> Or maybe I am being overly cautious again not to introduce any
> more unnecessary user confusion, and just should give them even
> longer rope to hang themselves.  I dunno.

Yes.

In the simplest version, branch.$name.push should only contain
the remote part of the refspec.  It should be symmetric to
branch.$name.merge.

So if branch.$name.push is set, "git push" means

    git push <url-from-remote> $name:<value of branch.$name.push>

This is what I proposed earlier.

	Steffen

Re: Adding push configuration to .git/config

[Johannes Schindelin]

Hi,

On Thu, 22 Nov 2007, Steffen Prohaska wrote:

> 	git checkout -b foo origin/master
>         work work work
> 	git checkout -b bar origin/master
> 	work work work
> 	git checkout foo
> 	git pull   # or git fetch; git rebase
> 	git push
> 	git checkout bar
> 	git branch -d foo
>         work work, ... and later push bar, too

I have to say that I slowly grow an antipathy for "git push" without 
parameters.  _All_ of the confusions with push that I saw stem from being 
too lazy to say where and what you want to push.  (Okay, there is this 
other thing where people say "git push origin master:master" and I still 
do not know where they got _that_ from.)

I would _never_ teach people to be sloppy here.  Even if you introduce 
whatever appears convenient to you.  IMHO this is not only giving rope, 
but close to putting the noose around the neck.

Ciao,
Dscho

Re: Adding push configuration to .git/config

[Junio C Hamano]

Johannes Schindelin <Johannes.Schindelin@gmx.de> writes:

> I have to say that I slowly grow an antipathy for "git push" without 
> parameters.  _All_ of the confusions with push that I saw stem from being 
> too lazy to say where and what you want to push.

The same thing can be said for "fetch" by the way.

Re: Adding push configuration to .git/config

[Andreas Ericsson]

Junio C Hamano wrote:
> Johannes Schindelin <Johannes.Schindelin@gmx.de> writes:
> 
>> I have to say that I slowly grow an antipathy for "git push" without 
>> parameters.  _All_ of the confusions with push that I saw stem from being 
>> too lazy to say where and what you want to push.
> 
> The same thing can be said for "fetch" by the way.

I disagree, since "fetch" at worst will auto-update the remote-tracking
branches only, while "push" may publish changes that are downright
wrong and never meant for publishing. What's worse is that fixing up
published history is a whole lot messier than it is to fix ones own
remote-tracking branches.

-- 
Andreas Ericsson                   andreas.ericsson@op5.se
OP5 AB                             www.op5.se
Tel: +46 8-230225                  Fax: +46 8-230231

Re: Adding push configuration to .git/config

[Steffen Prohaska]

On Nov 22, 2007, at 12:23 PM, Johannes Schindelin wrote:

> I have to say that I slowly grow an antipathy for "git push" without
> parameters.  _All_ of the confusions with push that I saw stem from  
> being
> too lazy to say where and what you want to push.  (Okay, there is this
> other thing where people say "git push origin master:master" and I  
> still
> do not know where they got _that_ from.)


I don't agree.  "git push" should support good defaults. At
some point you make the decision to publish, and you use
"git push" for this.  If you have a reasonably stable environment
there will be a good default, what publishing means.

Obviously users should think before they "git push".  They know
that they are publishing, and they (hopefully) understand
that they can't easily undo this operation.  But I believe
people who used any version control system before know that.
It's the same for every system.  If you publish, others can
get your source, and this can't easily be reverted.

But people are lazy, and having a good default is what they
expect from a good tool.  The default should be safe, and
reliably do something useful.  A good default can safe you
from typing errors.  But the default should not do too much,
and should not do unexpected things; at least not until you
explicitly configured.

You know that I believe the current default is not such a
choice.  Pushing matching branches sooner or later triggers
annoying errors if used with a shared remote repository.
But this is how the default is; and I'll live with it.

At least it saves me time.  I learnt to ignore the error
messages.  And we now have '--dry-run'.  So I can quickly
check what will happen.

But, I strongly believe that a tool that expects users to
type the current branch and the default remote each time;
just for publishing some changes to the default location,
is not what users want.

	Steffen

Re: Adding push configuration to .git/config

[Nico -telmich- Schottelius]

[-- Attachment #1: Type: text/plain, Size: 1549 bytes --]

Hello guys,

I'm replying a bit late, had much to work in the last days.

I really like some ideas discussed here and want to state that

- "git push" without options is much easier and does nothing wrong,
  if you configured the branch.$name.pushto correctly
- I also think that having support for multiple push destinations
  per branch would be excellent for a distributed version control system
  like git
- doing 'git push origin master:myremote/myname' just covers to much
  redundant data, which imho can (but not must) be put into .git/config
- I don't care about the configuration names, we can even stick to
  "merge" for now and add simply add "push" and rename them in git 2.x

I currently would like this variant mostly, allowing high flexibility:

--------------------------------------------------------------------------------
[remote "myremote"]
   url = git+ssh://.... # no change
   ref = refs/heads/    # renamed fetch = ...

# that way we can use the remote for fetch and push:

[branch "master"]
   merge = myremote
   push = myremote
   push = anotherremote

[branch "otherbranch"]
   merge = otherremote
   push = otherremote
   push = classmate
   push = myremote
--------------------------------------------------------------------------------

What do you think about that approach?

Sincerly

Nico

-- 
Think about Free and Open Source Software (FOSS).
http://nico.schottelius.org/documentations/foss/the-term-foss/

PGP: BFE4 C736 ABE5 406F 8F42  F7CF B8BE F92A 9885 188C

[-- Attachment #2: Digital signature --]
[-- Type: application/pgp-signature, Size: 189 bytes --]

Re: Adding push configuration to .git/config

[Johannes Schindelin]

Hi,

On Wed, 28 Nov 2007, Nico -telmich- Schottelius wrote:

> [branch "master"]
>    merge = myremote
>    push = myremote
>    push = anotherremote

This is not how the current config works.  "merge" specifies the remote 
ref name, "remote" specifies the remote.

So your proposal would imply breaking most existing setups.

Ciao,
Dscho

Re: Adding push configuration to .git/config

[Junio C Hamano]

Nico -telmich- Schottelius <nico-linux-git@schottelius.org> writes:

> ...
> [branch "otherbranch"]
>    merge = otherremote
>    push = otherremote
>    push = classmate
>    push = myremote
> --------------------------------------------------------------------------------
>
> What do you think about that approach?

Huh?

Is this a reinjection of an ancient message by some gateway?

You were already told branch.$name.merge has a defined meaning and
syntax, and you cannot make it refer to a remote shorthand without
breaking an existing setup.

Also if you want to have more than one destination repository for a
single push, I think that is already supported with remote.$name.url.

IIRC, there was a suggestion to enhance remote.$name configuration in
this way instead, so that you can use different URL for fetching and
pushing:

	[branch "foo"]
        remote = "there"
        merge = refs/heads/master

	[remote "there"]
        url = git://git.there.xz/repo.git
        push_url = git.there.xz:repo.git
        push_url = git.there.xz:backup.git
	fetch = refs/heads/*:refs/remotes/there/*

I further vaguely recall that the comments on the alternative were
positive (it might have been you who responded, or somebody else, I do
not remember).

Re: Adding push configuration to .git/config

[Jakub Narebski]

Junio C Hamano wrote:

> IIRC, there was a suggestion to enhance remote.$name configuration in
> this way instead, so that you can use different URL for fetching and
> pushing:
> 
>         [branch "foo"]
>         remote = "there"
>         merge = refs/heads/master
> 
>         [remote "there"]
>         url = git://git.there.xz/repo.git
>         push_url = git.there.xz:repo.git
>         push_url = git.there.xz:backup.git
>         fetch = refs/heads/*:refs/remotes/there/*
> 
> I further vaguely recall that the comments on the alternative were
> positive (it might have been you who responded, or somebody else, I do
> not remember).

If I remember correctly one of the suggestions was to allow for multiple
URLs, and for fetch use _first_ one that responds, for push use _all_
that are _possible_ to push to. Or at least support multiple url for
push; this way you would have to configure separate remote for fetch and
for push, but you would have to push only once to push to all repos.

But push_url, or pushURL seems like better idea, IMHO.

-- 
Jakub Narebski
Warsaw, Poland
ShadeHawk on #git

Re: Adding push configuration to .git/config

[MichaelTiloDressel]

On Nov 22, 2007, at 12:23 PM, Johannes Schindelin wrote:
>You know that I believe the current default is not such a
>choice.

To me the default is not very clear. I read somewhere (I wish I could
find where that was again)
that push will e.g. push all the remotes that do not contain a push line
by default 
(or maybe only in case the remote belonging to the current branch does
not contain a push?).

Anyway the way I try at the moment to have push by default only push the
current branch 
is by setting up a separate remote for each branch even if they belong
to the same remote
subdirectory. In addition I have a remote named origin which contains a
line:
push = nothing:nowhere
which creates an error for the default case that has no explicit remote.

My .git/config looks something like this:

[remote "origin"
        url = git+ssh://myuid@server/gitrepos/myprogit
        fetch = +refs/heads/master:refs/remotes/origin/master
        fetch =
+refs/heads/TopicA_v0.14_Branch:refs/remotes/origin/TopicA_v0.14_Branch
        fetch =
+refs/heads/mypro-v0.31_Branch:refs/remotes/origin/mypro-v0.31_Branch
        push = nothing:nowhere
[remote "master"]
        url = git+ssh://myuid@server/gitrepos/myprogit
        fetch = +refs/heads/master:refs/remotes/origin/master
        push = refs/heads/master:refs/heads/master
[remote "topicA"]
        url = git+ssh://myuid@server/gitrepos/myprogit
        fetch =
+refs/heads/TopicA_v0.14_Branch:refs/remotes/origin/TopicA_v0.14_Branch
        push =
refs/heads/TopicA_v0.14_Branch:refs/heads/TopicA_v0.14_Branch
[remote "mypro-v0.31"]
        url = git+ssh://myuid@server/gitrepos/myprogit
        fetch =
+refs/heads/mypro-v0.31_Branch:refs/remotes/origin/mypro-v0.31_Branch
        push =
refs/heads/mypro-v0.31_Branch:refs/heads/mypro-v0.31_Branch
[branch "master"]
        remote = master
        merge = refs/heads/master
[branch "mypro-v0.31_Branch"]
        remote = mypro-v0.31
        merge = refs/heads/mypro-v0.31_Branch
[branch "TopicA_v0.14_Branch"]
        remote = topicA
        merge = refs/heads/TopicA_v0.14_Branch


Cheers,
Michael