Update merge-main-into-feature-branch script#1420

Merged

jonsimantov merged 2 commits intomainfrom

update-merge-main-script

Aug 7, 2023

Commits on Aug 7, 2023

Before creating the merge-main PR, branch it off main, so merge conflicts can be addressed in the branch rather than by committing to main.
jonsimantov
committed
Format.
jonsimantov
committed