chore: CI: disable large runner again

This commit is contained in:
Sebastian Ullrich 2024-05-02 17:46:29 +02:00 committed by GitHub
parent 92fac419e7
commit 092ca8530a
No known key found for this signature in database
GPG key ID: B5690EEEBB952194

View file

@ -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}",