Check out PL code explicitly when building GitHub pages (#3917)

This fixes a breakage of the release job where the Javascript code that builds the K webpage is unable to find the PL tutorial code.
runtimeverification · Jan 19, 2024 · 1cb462c · 1cb462c
1 parent 464b2fc
commit 1cb462c
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
@@ -436,6 +436,12 @@ jobs:
           path: gh-pages
           token: ${{ secrets.JENKINS_GITHUB_PAT }}
           fetch-depth: 0
+      - name: 'Checkout PL Tutorial code'
+        uses: actions/checkout@v3
+        with:
+          repository: runtimeverification/pl-tutorial
+          path: gh-pages/k-distribution/pl-tutorial
+          token: ${{ secrets.JENKINS_GITHUB_PAT }}
       - working-directory: gh-pages
         run: |
           git config --global user.name rv-jenkins