Hi, I just uploaded a small change[1] for some code clean up. Someone needs to +2 it and I will push it :-)
Cheers, Murtadha [1] https://asterix-gerrit.ics.uci.edu/#/c/618/1 <https://asterix-gerrit.ics.uci.edu/#/c/618/1> > On Feb 5, 2016, at 6:31 PM, Till Westmann <[email protected]> wrote: > > Hi, > > the GitHub mirror is again not up to date (it’s at fa8a7ad while git-wip is > at a590763). > Does anybody have a small change to push a and trigger the mirroring? > > Cheers, > Till
