Merge pull request 'ci: run on the desktop runner (runs-on: desktop)' (#32) from ci/runs-on-desktop into main
This commit was merged in pull request #32.
This commit is contained in:
@@ -16,7 +16,7 @@ on:
|
||||
# cost and the evidence are in README's Development section.
|
||||
types: [opened, synchronize, reopened, edited]
|
||||
|
||||
# gitdan-ci runs four repos' CI on two capacity slots, and the compiler-backed
|
||||
# The desktop runner (gitdan#112) has few slots, and the compiler-backed
|
||||
# suites below are multi-minute. A superseded run costs a slot in front of
|
||||
# somebody's build, so drop it.
|
||||
#
|
||||
@@ -40,7 +40,7 @@ jobs:
|
||||
# no `pull_request` context, so `github.event.pull_request.draft` is empty
|
||||
# there and the negation alone would be unreliable. Never drop it.
|
||||
if: ${{ github.event_name != 'pull_request' || !github.event.pull_request.draft }}
|
||||
runs-on: ubuntu-latest
|
||||
runs-on: desktop
|
||||
timeout-minutes: 20
|
||||
# Deliberately no `container.volumes:` entry, unlike every repo that
|
||||
# CONSUMES this action. The suites below build throwaway workspaces under
|
||||
@@ -113,7 +113,7 @@ jobs:
|
||||
# job defers or misses.
|
||||
needs: selftest
|
||||
if: ${{ github.event_name == 'push' && github.ref == 'refs/heads/main' }}
|
||||
runs-on: ubuntu-latest
|
||||
runs-on: desktop
|
||||
timeout-minutes: 2
|
||||
# Requests write access from the run's built-in token -- whether that
|
||||
# grant actually lets it push here is unobserved until the first merge
|
||||
|
||||
@@ -20,7 +20,7 @@ concurrency:
|
||||
jobs:
|
||||
sweep:
|
||||
name: move v1 to main if it lags
|
||||
runs-on: ubuntu-latest
|
||||
runs-on: desktop
|
||||
timeout-minutes: 25
|
||||
permissions:
|
||||
contents: write
|
||||
|
||||
Reference in New Issue
Block a user