From c1f6daf1acda8738dc97fe69cc323d5ad0ecdbdd Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Wed, 29 Nov 2023 00:18:20 +1100 Subject: [PATCH] fix: remove unnecessary step in pr-release.yml (#2976) This step was unnecessary, as the script uses an unauthenticated https URL anyway, and apparently was causing a [permissions problem](https://github.com/leanprover/lean4/actions/runs/7005903162/job/19094622187#step:8:7). --- .github/workflows/pr-release.yml | 1 - 1 file changed, 1 deletion(-) diff --git a/.github/workflows/pr-release.yml b/.github/workflows/pr-release.yml index 8f4b31b3c6..63ee7e555c 100644 --- a/.github/workflows/pr-release.yml +++ b/.github/workflows/pr-release.yml @@ -84,7 +84,6 @@ jobs: id: most-recent-nightly-tag if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }} run: | - git remote add nightly https://foo:'${{ secrets.PUSH_NIGHTLY_TOKEN }}'@github.com/${{ github.repository_owner }}/lean4-nightly.git echo "MOST_RECENT_NIGHTLY=$(script/most-recent-nightly-tag.sh)" >> $GITHUB_ENV - name: 'Setup jq'