Persist credentials

This credential is required for `git push` later in the job.

diff --git a/.github/workflows/make-docs.yml b/.github/workflows/make-docs.yml
index f4f9614e06d272fef6463381b2d4b27c3982ecd2..5bcd1c9cfd98796f8d9122e364c05f3cdbab216c 100644 (file)
--- a/.github/workflows/make-docs.yml
+++ b/.github/workflows/make-docs.yml
@@ -15,8 +15,6 @@ jobs:
     runs-on: ubuntu-26.04
     steps:
       - uses: actions/checkout@v7
-        with:
-          persist-credentials: false
 
       - name: Build README.md
         shell: pwsh