Remove GitHub workflow metadata
ober
146654d906bb94e99284a0b977ba3b940fe169b0
deleted file mode 100644 --- a/.github/workflows/ci.yml +++ /dev/null @@ -1,36 +0,0 @@ -name: CI - -on: - push: - branches: [main, master] - pull_request: - workflow_dispatch: - -permissions: - contents: read - -jobs: - verify: - runs-on: ubuntu-latest - steps: - - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4 - with: - persist-credentials: false - - - name: Install build tools - run: sudo apt-get update && sudo apt-get install -y build-essential curl ca-certificates git openssh-client ripgrep - - - name: Install jerbuild - run: support/install-verified-jerbuild.sh /tmp/jerbuild - - - name: Build jerboa-treesitter - run: | - set -eu - support/fetch-locked-deps.sh dependency-lock.tsv .deps/jerboa-treesitter - JERBUILD=/tmp/jerbuild make -C .deps/jerboa-treesitter build - - - name: Verify - run: JERBUILD=/tmp/jerbuild JERBOA_TREESITTER_HOME=.deps/jerboa-treesitter make verify - - - name: Release evidence - run: JERBUILD=/tmp/jerbuild JERBOA_TREESITTER_HOME=.deps/jerboa-treesitter make release-evidence