user_id check only on scoring run #141
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: Sync develop with master | |
| 'on': | |
| pull_request: | |
| types: | |
| - closed | |
| branches: | |
| - master | |
| permissions: | |
| contents: write | |
| jobs: | |
| start: | |
| name: "Starting -🤞" | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Starting | |
| id: init | |
| run: | | |
| echo "Starting branch synchronization of ${{ github.repository }}" | |
| create_pr_for_nonplugin: | |
| name: Synchronizing non-plugin PR | |
| needs: start # This job now needs the 'start' job to complete first | |
| if: > | |
| github.event.pull_request.merged == true && | |
| !(startsWith(github.event.pull_request.head.ref, 'web_submission_') && | |
| contains(github.event.pull_request.title, 'brain-score.org submission')) | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Check out the develop branch | |
| uses: actions/checkout@v3 | |
| with: | |
| fetch-depth: 0 # Fetch full history | |
| ref: develop | |
| - name: Reset the develop branch | |
| run: | | |
| git fetch origin master | |
| git reset --hard origin/master | |
| - name: Get commit summary | |
| id: commit_summary | |
| run: | | |
| git log -1 --pretty=format:"%s" | |
| echo "::set-output name=summary::$(git log -1 --pretty=format:"%s")" | |
| - name: Create pull request in develop | |
| uses: peter-evans/create-pull-request@v6 | |
| with: | |
| token: '${{ secrets.PAT }}' | |
| commit-message: Sync master into develop | |
| title: Sync master into develop. Triggered by PR #${{ github.event.pull_request.number }} | |
| body: >- | |
| This PR syncs the latest changes from the master branch into the | |
| develop branch. | |
| Commit Summary: ${{ steps.commit_summary.outputs.summary }} | |
| base: develop | |
| branch: 'developer-sync-pr-${{ github.event.pull_request.number }}' | |
| auto_sync_for_plugin: | |
| needs: start | |
| if: > | |
| github.event.pull_request.merged == true && | |
| startsWith(github.event.pull_request.head.ref, 'web_submission_') && | |
| contains(github.event.pull_request.title, 'brain-score.org submission') | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Checkout the develop branch | |
| uses: actions/checkout@v3 | |
| with: | |
| fetch-depth: 0 | |
| ref: develop | |
| - name: Configure Git user | |
| run: | | |
| git config --global user.name "Branch Synchronizer" | |
| git config --global user.email "[email protected]" | |
| - name: Ensure develop branch is updated | |
| run: | | |
| git fetch origin develop | |
| git checkout develop | |
| git merge origin/develop | |
| # Fetch latest change from master, checkout develop, merge changes from master to develop. | |
| # Includes conflict handling | |
| - name: Merge master into develop | |
| id: merge | |
| run: | | |
| git fetch origin master | |
| git checkout develop | |
| git merge origin/master || { | |
| if git diff --name-only --diff-filter=U | grep -q '.'; then | |
| echo "Merge conflict detected" | |
| echo "::set-output name=merge_conflict::true" | |
| else | |
| echo "Merge failed due to another reason" | |
| exit 1 | |
| fi | |
| } | |
| - name: Push changes to develop (if merge is successful) | |
| if: steps.merge.outcome == 'success' | |
| run: | #Use force-with-lease to prevent accidental overwrite if branch has been updated. If fails, rebase the update and retry | |
| git push origin develop --force-with-lease || { | |
| echo "Push failed due to updates in develop. Attempting to rebase and retry..." | |
| git fetch origin develop | |
| git rebase origin/develop | |
| git push origin develop --force-with-lease | |
| } | |
| - name: Get commit summary | |
| id: commit_summary | |
| run: | | |
| git log -1 --pretty=format:"%s" | |
| echo "::set-output name=summary::$(git log -1 --pretty=format:"%s")" | |
| - name: Create pull request for merge conflicts | |
| if: steps.merge.outputs.merge_conflict == 'true' | |
| uses: peter-evans/create-pull-request@v6 | |
| with: | |
| token: '${{ secrets.PAT }}' | |
| commit-message: Merge master into develop with conflict resolution | |
| title: Resolve conflicts between master and develop. Triggered by PR #${{ github.event.pull_request.number }} | |
| body: | | |
| This PR resolves merge conflicts between master and develop. | |
| Commit Summary: ${{ steps.commit_summary.outputs.summary }} | |
| base: develop | |
| branch: 'developer-sync-pr-conflict-${{ github.event.pull_request.number }}' | |
| - name: Handle other merge failures | |
| if: failure() && steps.merge.outputs.merge_conflict != 'true' | |
| run: > | |
| echo "Handle non-conflict related failure, such as network issues or missing branches" | |
| # Possibly incorporate additional handling logic here (e.g.,notifications or retries) | |
| no_changes: | |
| name: "No Changes Made. No synchronization needed." | |
| needs: start | |
| if: > | |
| ( | |
| needs.create_pr_for_nonplugin.result != 'success' && | |
| needs.auto_sync_for_plugin.result != 'success' | |
| ) | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Echo no changes | |
| run: echo "No changes were made to master branch 👍" |