Hi, I just pushed some changes, that seem to revert part of the changes done to GitHub.
This is not an expression of them being unwanted, but more a necessary thing in order to re-sync both repos without having to force anything. Hopefully I can now re enable the sync mechanism and we’ll be able to continue from there on. Chris
