Hi, I accidentally pushed to the master branch, a coverity fix that
was already fixed in develop :/

What should we do? Force-push back the old master? Or just let it lie there?

-- 

Saludos,
Felipe Sateler

------------------------------------------------------------------------------
_______________________________________________
Csound-devel mailing list
Csound-devel@lists.sourceforge.net

I took a look and my vote is to just leave it in master.  It seems
harmless, and I don't imagine anyone will be affected by the one
character change in that commit if they are building from master.
We're planning a new release soon so master will advance soon anyways
when we merge 6.06.0 into it.

steven

On Mon, Sep 21, 2015 at 7:15 PM, Felipe Sateler  wrote:
> Hi, I accidentally pushed to the master branch, a coverity fix that
> was already fixed in develop :/
>
> What should we do? Force-push back the old master? Or just let it lie there?
>
> --
>
> Saludos,
> Felipe Sateler
>
> ------------------------------------------------------------------------------
> _______________________________________________
> Csound-devel mailing list
> Csound-devel@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/csound-devel

------------------------------------------------------------------------------
_______________________________________________
Csound-devel mailing list
Csound-devel@lists.sourceforge.net