Closed NoahCardoso closed 1 week ago
Sorry, I noticed that this is a different branch than the source of #3794. Can you explain what the differences are? Can we delete the previous branch, the one used for #3794 ?
The other branch had 40 merge conflicts with the main
branch and I didn't know which commits to keep. It was easier for me to cherry-pick my commits onto a new branch that was based on the current version of main
. #3794 can be deleted.
Closes #3153