summaryrefslogtreecommitdiff
path: root/.github/workflows
diff options
context:
space:
mode:
authorTom Kelly <ctk21@cl.cam.ac.uk>2021-03-03 13:30:53 +0000
committerTom Kelly <ctk21@cl.cam.ac.uk>2021-03-03 13:30:53 +0000
commit701bbb9b00c3a0f2d48523a2bb2d42db3f64309b (patch)
tree150e1bbdb54d56b01a0f351dc68510ce4b71befe /.github/workflows
parentbcbaccf22afcbd76ace9e8a6803d4db3a7aeb731 (diff)
parente717512a54349bce4bbbb9590d4fe5a2c671c4e9 (diff)
downloadocaml-701bbb9b00c3a0f2d48523a2bb2d42db3f64309b.tar.gz
Merge commit 'e717512a54349bce4bbbb9590d4fe5a2c671c4e9' into parallel_minor_gc_4_12
Diffstat (limited to '.github/workflows')
-rw-r--r--.github/workflows/stale.yml2
1 files changed, 1 insertions, 1 deletions
diff --git a/.github/workflows/stale.yml b/.github/workflows/stale.yml
index 62e4864f69..27d63bfd3d 100644
--- a/.github/workflows/stale.yml
+++ b/.github/workflows/stale.yml
@@ -7,7 +7,7 @@ jobs:
stale:
runs-on: ubuntu-latest
steps:
- - uses: actions/stale@v2
+ - uses: actions/stale@v3
with:
repo-token: ${{ secrets.GITHUB_TOKEN }}
stale-issue-message: 'This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc.'