Re: Personal branches and restrictions with GIT repository

[Joel Brobecker <brobecker@adacore.com>]

> Yeah I think this is the question really. And to reiterate not talking
> about Master here, just personal branches. Are we free (in the case of
> a merge commit to a personal branch), to ignore the hook and commit
> anyway? Is it a suggestion or a directive? That's the crux of the
> matter.
> 
> I've not checked the wiki yet. Maybe some guidelines for personal
> branches and/or master branches would be ideal. I'll volunteer to get
> one started if nobody else does. Just need to know the said guidelines
> first ;)

No one else really provided any opinion so far. Although I would prefer
if personal branches were to follow the standard practices, I do not
have a particularly strong opinion on that. So let's give it another
couple of weeks, and if there are still no opinion, I will let you
chose and document the policy for personal branches.

-- 
Joel