Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
21 changes: 21 additions & 0 deletions .github/bin/retry
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
#!/usr/bin/env bash

set -euo pipefail

x() {
echo "+ $*" >&2
"$@"
}

max_retry_time_seconds=$(( 30 * 60 ))
retry_delay_seconds=10

END=$(( $(date +%s) + ${max_retry_time_seconds} ))

while (( $(date +%s) < $END )); do
x "$@" && exit 0
sleep "${retry_delay_seconds}"
done

echo "$0: retrying [$*] timed out" >&2
exit 1
83 changes: 83 additions & 0 deletions .github/workflows/milestone.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,83 @@
name: milestone

on:
push:
branches: [main]

defaults:
run:
shell: bash --noprofile --norc -euo pipefail {0}

jobs:
set-milestone:
if: github.repository_owner == 'trinodb'
runs-on: ubuntu-latest
steps:
- name: Checkout code
uses: actions/checkout@v4
- name: Get milestone from pom.xml
run: |
.github/bin/retry ./mvnw -v
Comment thread
mosabua marked this conversation as resolved.
MILESTONE_NUMBER="$(./mvnw help:evaluate -Dexpression=project.version -q -DforceStdout | cut -d- -f1)"
echo "Setting PR milestone to ${MILESTONE_NUMBER}"
echo "MILESTONE_NUMBER=${MILESTONE_NUMBER}" >> $GITHUB_ENV
- name: Set milestone to PR
uses: actions/github-script@v7
with:
github-token: ${{secrets.GITHUB_TOKEN}}
script: |
// Get pull request number from commit sha
// 'listPullRequestsAssociatedWithCommit()' lists the merged pull request
// https://docs.github.com/en/rest/reference/repos#list-pull-requests-associated-with-a-commit
// and https://octokit.github.io/rest.js/v19#repos-list-pull-requests-associated-with-commit
const pr_response = await github.rest.repos.listPullRequestsAssociatedWithCommit({
owner: context.repo.owner,
repo: context.repo.repo,
commit_sha: context.sha
})
if (pr_response.data.length === 0) {
console.log('Pull request not found for commit', context.sha)
return
}
if (pr_response.data.length > 1) {
console.log(pr_response.data)
throw 'Expected 1 pull request but found: ' + pr_response.data.length
}
const pr_number = pr_response.data[0].number
console.log('Found pull request', pr_number, 'for commit', context.sha)

// Get milestone
const {
MILESTONE_NUMBER
} = process.env
console.log('Milestone number to set', MILESTONE_NUMBER)

// Find milestone with matching title
// See https://octokit.github.io/rest.js/v19#pagination
const milestones = await github.paginate(github.rest.issues.listMilestones, {
owner: context.repo.owner,
repo: context.repo.repo,
state: 'all'
})
let milestone = milestones.find(milestone => milestone.title === MILESTONE_NUMBER)
console.log('Found milestone with title', MILESTONE_NUMBER, milestone)

// Create new milestone if it doesn't exist
if (!milestone) {
const create_response = await github.rest.issues.createMilestone({
owner: context.repo.owner,
repo: context.repo.repo,
title: MILESTONE_NUMBER
})
milestone = create_response.data
console.log('Created new milestone with title', MILESTONE_NUMBER, milestone)
}

// Set milestone to PR
await github.rest.issues.update({
owner: context.repo.owner,
repo: context.repo.repo,
milestone: milestone.number,
issue_number: pr_number
})
console.log('Added PR', pr_number, 'to milestone', MILESTONE_NUMBER)