Merge remote-tracking branch 'origin/develop'

runtimeverification · Jan 19, 2024 · 3eb8d8a · 3eb8d8a
2 parents bd81862 + 1cb462c
commit 3eb8d8a
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