Remove GitHub workflow metadata
ober
65b7e7cae36859e1e5077cfece674a44847fec88
deleted file mode 100644 --- a/.github/workflows/ci.yml +++ /dev/null @@ -1,41 +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.3.1 - with: - persist-credentials: false - - - name: Install build tools - run: sudo apt-get update && sudo apt-get install -y build-essential curl ca-certificates git ripgrep pkg-config - - - name: Fetch locked source dependencies - run: sh support/fetch-locked-deps.sh - - - name: Build locked Jerboa toolchain - run: make -C .deps/jerboa jerboa - - - name: Verify - run: make verify - env: - JERBUILD: ${{ github.workspace }}/.deps/jerboa/dist/jerbuild - JERBOA_HOME: ${{ github.workspace }}/.deps/jerboa - JERBOA_SINATRA: ${{ github.workspace }}/.deps/jerboa-sinatra - - - name: Release evidence - run: make release-evidence - env: - JERBUILD: ${{ github.workspace }}/.deps/jerboa/dist/jerbuild - JERBOA_HOME: ${{ github.workspace }}/.deps/jerboa - JERBOA_SINATRA: ${{ github.workspace }}/.deps/jerboa-sinatra