> On Apr 13, 2017, at 12:31 PM, Kong, Fande <[email protected]> wrote: > > Hi Developers, > > Do we increase the patch number when pushing a new patch into maint? If not, > how to know if the current maint is different from the one I just got > yesterday. I know a commit number is always available.
One uses the git commit (or git log). > > Fande,
