Closed tocic closed 1 year ago
Merging #131 (0d30d09) into main (c0a910c) will not change coverage. The diff coverage is
100.00%
.
Seems like I don't have the rights to merge. There's no "Merge pull request" button in the UI, and this is my cmd output:
$ git push -vv
Pushing to github.com:cschreib/snitch.git
Enter passphrase for key '/home/tocic/.ssh/github_tocic':
ERROR: Permission to cschreib/snitch.git denied to tocic.
fatal: Could not read from remote repository.
Please make sure you have the correct access rights
and the repository exists.
I see, looks like you'd need to be formally invited as collaborator before you are able to do this. I've opened a ticket to discuss the topic (https://github.com/cschreib/snitch/issues/132), please chime in there if you have an opinion. In the meantime I will merge this myself, thanks for your contribution!
Closes #112.