Re: [boost] git reset and force push

On Tue, Oct 6, 2015 at 7:56 PM, Raffi Enficiaud < raffi.enficiaud@mines-paris.org> wrote:

Hi all,

Is there any policy wrt. reseting a branch master/develop and force pushing? The side question is to know if the boost git tools (the bot for submodules) can cope with those operations.

Thanks, Raffi

Are you trying to remove/hide something from the history? Unless it was a largish binary file added by mistake, why would you need to do that? If you want to remove commit(s) that have been published "git revert" should do it. The interim changes will be shown in the history, so force pushing won't be necessary. Lee