Merged and mirror back in sync :-)
> On Feb 5, 2016, at 7:15 PM, Till Westmann <[email protected]> wrote:
>
> Done. Let's hope it passes the tests :)
>
>> On Feb 5, 2016, at 19:02, Murtadha Hubail <[email protected]> wrote:
>>
>> 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
>>
