@Pierre Jouvelot please let's discuss here to continue https://github.com/math-comp/math-comp/pull/881#issuecomment-1122222883
Could you please do git remote -v
Here it is, but I don't want to waste your time with git issues. I'll try to do a clean PR later on :)
[nix-shell:~/Desktop/ownCloud/Github/pierre/math-comp]$ git remote -v
origin git@github.com:jouvelot/math-comp.git (fetch)
origin git@github.com:jouvelot/math-comp.git (push)
Thanks again for your kind help.
ok so you clearly miss a remote for the upstream development of mathcomp, without which you cannot keep in sync with the ongoing development (including your own), you must git remote add upstream git@github.com:math-comp/math-comp.git
to start with
Also you should never start from a branch you already used to develop another PR (unless you really know why)
Thanks, Cyril. I had created a new branch, and moved into it, but this didn't work as I thought it would. I'm going to try with your suggestions, and resubmit.
You do not need to do anything, since I reopened you PR, did the rebase and commited my suggestions
Last updated: Oct 13 2024 at 01:02 UTC