Re: Personal branches and restrictions with GIT repository

[Joel Brobecker <brobecker@adacore.com>]

> So this boils down to two questions:
> 
> 1) Do we need this hook for personal branches?

It's a hook aimed at users who are not very familiar with git
and who might accidently do a merge instead of a rebase.
Un understand that this can be felt as a PITA for more experienced
git users, but it is a really easy mistake to make when one is not
paying attention, and it is also quickly resolved.

> 
> 2) And are users allowed to do whatever they want in their own
>    personal branch (within sane defaults)?

To answer your two questions, I think it boils down to policy
rather than need. The hooks should accomodate the policy.

We can turn all pre-commit checks for user-branches. I don't believe
that the hooks, as currently implemented, support turning off just
that "accidental merge" check. The latter can, of course, be easily
implemented.

FWIW, my take is that if you're going to have your branch hosted
on the sourceware git, it's not a big effort to be following the same
guidelines as other official branches. But if people want it otherwise,
then we can adjust the hooks.

-- 
Joel