mirror/gradio
2
0
Fork 0
mirror of https://github.com/gradio-app/gradio.git synced 2024-11-27 01:40:20 +08:00
Code Issues Packages Projects Releases Wiki Activity

remove obsolete run circleci script (#4416)

Browse Source
This commit is contained in:
2-5 2023-06-05 02:18:59 +00:00 committed by GitHub
parent 2effd86353
commit d13e889813
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 0 additions and 20 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
scripts/helpers.sh
View File

@ -51,17 +51,6 @@ function pnpm_required() {
program_required "pnpm" "https://pnpm.io/7.x/installation"
}
#######################################
# Check for the CircleCI program.
# Arguments:
# None
# Outputs:
# None
#######################################
function circleci_required() {
program_required "circleci" "https://circleci.com/docs/1.0/local-cli/"
}
#######################################
# Check for the AWS CLI program.
# Arguments:

9
scripts/run_circleci.sh
View File

@ -1,9 +0,0 @@
#!/bin/bash
cd "$(dirname ${0})/.."
source scripts/helpers.sh
circleci_required
echo "Running CircleCI locally..."
circleci local execute