Closed fchapoton closed 6 years ago
based on my 2 other pending pull requests.
First time I've used GitHub's online merge conflict resolution. Quite nice, especially for very minor conflicts like this one.
based on my 2 other pending pull requests.