external
/
citus
mirror of https://github.com/citusdata/citus.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Disable CircleCI

pull/7276/head
Gokhan Gulbiz 2023-10-25 15:54:32 +03:00
parent 10198b18e8
commit 790dca08bc
No known key found for this signature in database
GPG Key ID: 608EF06B6BD1B45B
2 changed files with 3 additions and 1131 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1128
.circleci/config.yml
View File

File diff suppressed because it is too large Load Diff

6
ci/check_all_ci_scripts_are_run.sh
View File

@ -11,11 +11,11 @@ source ci/ci_helpers.sh
ci_scripts=$(
find ci/ -iname "*.sh" |
sed -E 's#^ci/##g' |
grep -v -E '^(ci_helpers.sh|fix_style.sh)$'
grep -v -E '^(ci_helpers.sh|fix_style.sh|check_enterprise_merge.sh)$'
)
for script in $ci_scripts; do
if ! grep "\\bci/$script\\b" .circleci/config.yml > /dev/null; then
echo "ERROR: CI script with name \"$script\" is not actually used in .circleci/config.yml"
if ! grep "\\bci/$script\\b" -r .github > /dev/null; then
echo "ERROR: CI script with name \"$script\" is not actually used in .github folder"
exit 1
fi
if ! grep "^## \`$script\`\$" ci/README.md > /dev/null; then