Closed ayush9pandey closed 1 year ago
Those are great ideas! The repo is now public. Would you like to make the changes before we merge this PR?
The system doesn't let me approve the request due to merge conflicts. Could you please merge main?
I don't see merge conflicts. I have added codecov to github actions but will need to merge to main before it starts working (I think). So let's merge this PR then?
Two tasks at hand right now:
I agree we should merge it, but there seems to be a problem with the branch. See below. The merge button is disabled. This seems relevant: https://stackoverflow.com/questions/50012036/github-cant-rebase-my-feature-branch-this-branch-cannot-be-rebased-due-to-con
Hi @ayush9pandey, the following set of commands worked for me:
$ git checkout badges
$ git fetch
$ git merge origin/main
$ git reset --soft origin/master
$ git commit -va
$ git push -f
I pushed those commands to this branch, but it erases history. Would you like to push your changes from another branch, so that this appears as your commit?
Odd.. I don't see this issue
The
pacti_development
action is failing so the badge displays that it is failing but that should not stop us from merging the PR.The code coverage badge will work when we integrate Pacti with Codecov. As far as I know, Codecov works for free for open-source repos. Same for Google Colab badge, we can create a Google Colab launch link which will let users quickly run the code with one-click. So, if we want, we can wait and merge this PR once the repo is public. What do you think @iincer?