Closed ChienYungChi closed 1 month ago
awaiting-review
@ChienYungChi : Can you check and resolve the merge conflicts. In all likelihood, merging the main
branch into your PR should fix it.
@ChienYungChi was the PR closing accidental? If yes, then it can be re-opened
Hi, I resolved the conflict and proposed a new PR. I don’t know if the closing was accidental. I didn't know about the closing until you told me.
You don't need to close a PR when resolving a merge conflict. I have linked yoir new PR. It is now in the review queue. Since I am manually moving PRs around for now, I apologise for delays in this process.
OK. I didn’t know that I could resolve that in the same PR, so I created another one. I didn’t close the old PR myself. Maybe it was closed because I discarded a commit in my fork before creating the new commit. Next time I will just add commits instead of discarding old ones first. I apologize for this inconvenience.
This corresponds to issue "SUBGRAPH: Prove that 38 and 42 are equivalent."