Done (although possibly we should note to use git and not iceberg to merge the branch?)
> On 10 May 2018, at 01:54, Bernardo Ezequiel Contreras <[email protected]> > wrote: > > > > On Wed, May 9, 2018 at 9:36 PM, Tim Mackinnon <[email protected] > <mailto:[email protected]>> wrote: > > I also wasn’t sure how you merge a branch back on to master with Iceberg (can > you ?) - so I just did that bit in gitlab. > > > no, i didn't use iceberg. i just run the script (without the push at the end) > and then i use git commands to get back to master > and merge the migrate-sources-to-tonel branch. and then i pushed to origin. > > if you have a better script, just propose the fix in github. there's a pencil > in the left hand > with the caption 'Fork this project and edit this file' after the > modification you have the > option to create a pull request. > > > -- > Bernardo E.C. > > Sent from a cheap desktop computer in South America.
