Re: [Archer] Remote repository and git push command

[Joel Brobecker <brobecker@adacore.com>]

>   If I make change to my branch, but also want to rebase my branch to
>   current HEAD, I get a warning about "loosing history" when I try to
>   push the new version onto the remote repository.

That's the disadvantage of using rebase.  Rebase is great because
it keeps the history linear.  But the downside is that it makes it
more difficult for others to track and make changes on top of your
branch.

> It is allowed to force the push in that case or how should I proceed
> to avoid the "losing history" complaint.

I don't know what the policy is on the Archer branch, or whether
there is one or not.

Given that you are doing the work using git mostly to be able to
maintain a set of patches, I think that you would really benefit
from using rebasing, rather than merging.  As there is no one
else pushing changes on that branch, it shouldn't have any impact
on anyone else.

Anyone more actively maintaining the Archer repo should be able
to give you the final OK (or not).

-- 
Joel