diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index ca10235caa..2de8d37979 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -56,8 +56,8 @@ jobs: const quick = ${{ steps.set-quick.outputs.quick }}; console.log(`quick: ${quick}`); // use large runners outside PRs where available (original repo) - // for now Windows only, which is the slowest non-debug job - let large = ${{ github.event_name != 'pull_request' && github.repository == 'leanprover/lean4' }} ? "-large" : ""; + // disabled for now as this mostly just speeds up the test suite which is not a bottleneck + // let large = ${{ github.event_name != 'pull_request' && github.repository == 'leanprover/lean4' }} ? "-large" : ""; let matrix = [ { // portable release build: use channel with older glibc (2.27) @@ -138,7 +138,7 @@ jobs: }, { "name": "Windows", - "os": `windows-2022${large}`, + "os": "windows-2022", "release": true, "quick": false, "shell": "msys2 {0}",