mirror of
https://gitflic.ru/project/openide/openide.git
synced 2026-09-27 10:03:11 +07:00
Sebastiano Poggi
3db404b9bb
This cleans up a number of small issues with the scripts:
* Release notes script
* Ensure it's run from the `jewel` folder
* Add support for nested release note bullet points
* Add warnings when there are "orphan" Jewel commits have no
matching PR information attached
* Fix a number of bugs
* Fix version number in release notes doc to work with script
* Extract common checks from other scripts to utils.sh
* Temporarily remove the ability to post PR comments as it won't work
across forks anyway
closes https://github.com/JetBrains/intellij-community/pull/3177
GitOrigin-RevId: c7c51779b65c4d3b6ee5f002356be7cb2f56f80a
43 lines
1.0 KiB
Bash
43 lines
1.0 KiB
Bash
#!/usr/bin/env bash
|
|
|
|
echoerr() {
|
|
local message=$*
|
|
echo -e "\033[0;31m$message\033[0m" 1>&2
|
|
}
|
|
|
|
echowarn() {
|
|
local message=$*
|
|
echo -e "\033[1;33m$message\033[0m" 1>&2
|
|
}
|
|
|
|
# Function to post a comment to the PR and exit.
|
|
# It uses the gh CLI, which is pre-installed on GitHub-hosted runners.
|
|
# The GITHUB_TOKEN and PR_NUMBER are provided by the workflow.
|
|
fail_check() {
|
|
local message=$1
|
|
echoerr "$message"
|
|
|
|
# TODO figure out how to reliably post comments to PRs from forks
|
|
# if [[ -n "$PR_NUMBER" && -n "$GITHUB_TOKEN" ]]; then
|
|
# if ! gh pr comment "$PR_NUMBER" --body "$message"; then
|
|
# echowarn "Failed to post comment to PR #$PR_NUMBER. Continuing..."
|
|
# fi
|
|
# else
|
|
# echowarn "PR_NUMBER or GITHUB_TOKEN not set, skipping posting PR comment."
|
|
# fi
|
|
}
|
|
|
|
check_gh_tool() {
|
|
if ! command -v gh &>/dev/null; then
|
|
echoerr "ERROR: The GitHub CLI (gh) is not installed. Please install it to continue."
|
|
exit 1
|
|
fi
|
|
}
|
|
|
|
check_pr_number() {
|
|
if [ -z "$PR_NUMBER" ]; then
|
|
echoerr "ERROR: PR_NUMBER environment variable not set."
|
|
exit 1
|
|
fi
|
|
}
|