Re: How to update a remote branch (remotes/origin/dev/guile-v2-work)

[Thomas Morley]

2018-06-08 0:36 GMT+02:00 David Kastrup <address@hidden>:
> Thomas Morley <address@hidden> writes:
>
>> One additional question: If I want to add something to the then
>> updated branch, would
>> $ git push origin HEAD:dev/guile-v2-work
>> work or would I need to follow the route you described above?
>
> As long as you don't rebase, your followup work is a descendant of the
> previous work and can be pushed without deletion.
>
> --
> David Kastrup

Ok
I'll check for `make doc' tomorrow and, if successful, will push the
rebased branch afterwards.

Thanks again,
  Harm