Re: Pushing to nofib

2022-09-27 Thread Sebastian Graf
Hi Simon, Similar to the policy for the main GHC repo, you have to push to a wip/ branch (or your personal fork) and then open a MR against the NoFib repo. Fortunately, the quality requirements for NoFib aren't high and it's likely your MR can be merged instantly. Cheers, Sebastian --

Pushing to nofib

2022-09-27 Thread Simon Peyton Jones
Friends How do I push to the nofib/ repository? I just wanted to add some documentation. I'm on branch 'master' and tried to push. Got this below. What next? Thanks Simon bash$ git push Enumerating objects: 5, done. Counting objects: 100% (5/5), done. Delta compression using up to 24 threads