From 1cb462c8ca19ad4c407cf82999e44955f7ce9d31 Mon Sep 17 00:00:00 2001
From: Bruce Collie <brucecollie82@gmail.com>
Date: Fri, 19 Jan 2024 17:04:05 +0000
Subject: [PATCH] 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.
---
 .github/workflows/release.yml | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
index 731a14ca624..5f33c491099 100644
--- 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