Hi,

here’s a small change [1] to get the GitHub mirror going again.
Please review and commit (if the tests work …).

Cheers,
Till


[1] https://asterix-gerrit.ics.uci.edu/#/c/787/

Reply via email to