github_merge: add option --all to merge all PR