Skip to content

Add additional keyboard shortcuts (#1839) #536

Add additional keyboard shortcuts (#1839)

Add additional keyboard shortcuts (#1839) #536

Workflow file for this run

name: Merge community changes into pro repo
on:
push:
branches:
- master
jobs:
updateFork:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v3
with:
repository: tiny-pilot/tinypilot-pro
token: ${{ secrets.PR_BOT_PAT }}
- name: Reset the default branch with upstream changes
run: |
git remote add upstream https://github.com/tiny-pilot/tinypilot.git
git fetch upstream master:upstream-master
git reset --hard upstream-master
- name: Get the URL of the original community PR
run: |
set -ux
COMMUNITY_PR_URL="$(curl \
--silent \
--show-error \
https://api.github.com/repos/tiny-pilot/tinypilot/commits/${{ github.sha }}/pulls?per_page=1 | \
jq \
--raw-output \
'.[0].html_url | select (.!=null)')"
readonly COMMUNITY_PR_URL
echo "COMMUNITY_PR_URL=${COMMUNITY_PR_URL}" >> "${GITHUB_ENV}"
- name: Create Pull Request
uses: peter-evans/create-pull-request@v4
with:
token: ${{ secrets.PR_BOT_PAT }}
branch: community-changes-${{ github.sha }}
delete-branch: true
# If the committer to the community repo (github.actor) has no access
# to the pro repo, the PR will be unassigned.
assignees: ${{ github.actor }}
reviewers: ${{ github.actor }}
title: Merge changes from community repository
body: |
Related ${{ env.COMMUNITY_PR_URL }}
@${{ github.actor }}, please merge [your changes from the Community repository](https://github.com/tiny-pilot/tinypilot/commit/${{ github.sha }}):
1. Update this branch with latest `master`
- If there are merge conflicts, it’s best to resolve them locally.
1. Check whether you need to make any Pro-specific adjustments to the code
1. Review and approve your changes
- You usually do this yourself. In case you had to make non-trivial adjustments, it’s also okay to request a proper peer review.
1. Set the merge style to “Create a merge commit” (regular merge)
- **Do not use “Squash and merge”!** If you accidentally squash, it’s not a disaster, but it will create a bit of noise on the subsequent PR from Community.
- We want a regular merge to preserve the commit history from Community
1. Merge the PR
Note that Github remembers the merge style of your last PR in this repo, so for your next “regular” PR, you may have to manually set it to “Squash and merge” again.