Adding a dependency to an existing PR

Stream: new members

[Stuart Presnell]

I have a beginner's GitHub question. Sorry if this is something super obvious.

I've submitted a PR (#10540) in which I add the file data/nat/prime_factorization. In responding to a reviewer suggestion I proved a lemma factors_count_pow and used it in a subsequent proof. But factors_count_pow properly belongs in data/nat/prime, not in this new file. No problem, I think, I'll just open a new PR (#10554) to submit factors_count_pow to data/nat/prime, and then I can make #10540 dependent on that by adding the comment - [ ] depends on: #10554. But now when I open data/nat/prime_factorization in VS Code the relevant lemma complains: unknown identifier 'factors_count_pow'. What do I need to do to tell VS Code that this branch now depends on another branch?

[Johan Commelin]

@Stuart Presnell You can merge one branch into the other. If branch foo depends on bar, then do

git checkout foo
git merge bar
git push

[Johan Commelin]

If you get merge conflicts, resolve them in VScode, add the resolved files, and commit the result.