summaryrefslogtreecommitdiff
path: root/.github/workflows
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@college-de-france.fr>2020-06-08 08:45:39 +0200
committerXavier Leroy <xavier.leroy@college-de-france.fr>2020-06-08 08:45:39 +0200
commitde21dafe28b319c6fd9881d28f031f41faa14a97 (patch)
tree08a63c758f01ca904853d1b6a4f6dbbc6afe1de0 /.github/workflows
parent06cabea1df6437e5bf4f8c6a63ecddb75bdf881e (diff)
downloadocaml-de21dafe28b319c6fd9881d28f031f41faa14a97.tar.gz
Upgrade the "stale" script to v3
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.'