Add missing permission to publish doc.

Also merged the build and publish doc into one job.

diff --git a/.github/workflows/makefile.yml b/.github/workflows/makefile.yml
index f83bab255a87158c0a160e8cf5e0974f37d66f56..23e0fa1fc16fa567290e573f88578210da6dce13 100644 (file)
--- a/.github/workflows/makefile.yml
+++ b/.github/workflows/makefile.yml
@@ -6,8 +6,11 @@ on:
   pull_request:
     branches: [ "master" ]
 
+permissions:
+  id-token: write
+
 jobs:
-  build_doc:
+  build_and_publish_doc:
 
     runs-on: ubuntu-latest
 
@@ -36,11 +39,6 @@ jobs:
         # Duration after which artifact will expire in days.
         retention-days: 7 # optional, default is 1
 
-  deploy_doc:
-
-    runs-on: ubuntu-latest
-
-    steps:
     - name: Deploy GitHub Pages site
       uses: actions/deploy-pages@v1.2.9
       #with: