Closed piklprado closed 9 years ago
PR #2 had conflicts. Merged manually in my branch and submitted in this PR.
No longer necessary; Chalom has fixed the conflicts meanwhile.
OK, maybe we need to use the github "assignees" more to flag who's working on each problem, so we avoid duplicating efforts.
PR #2 had conflicts. Merged manually in my branch and submitted in this PR.