Closed ia0 closed 7 years ago
Oops. I actually forgot Github used to create a merge commit even when not necessary. The common submodule misses the merge commit of https://github.com/Fruneau/libcommon/pull/8. I don't know if it's useful to update it or not.
This is not an actually issue in that specific case since there is no concurrent PR on the repo.
This PR should be merged only after https://github.com/Fruneau/libcommon/pull/8 is merged without modifications.