Skip to content

Fix broken links

Fix broken links #306

Workflow file for this run

name: PR Preview Workflow
on:
pull_request_target:
types:
- opened
- synchronize
- closed
concurrency:
group: docs
jobs:
build-and-preview:
if: github.event.action == 'opened' || github.event.action == 'synchronize'
runs-on: ubuntu-latest
steps:
- name: Checkout
uses: actions/checkout@v4
with:
ref: ${{ github.event.pull_request.head.sha }}
- name: Setup Julia
uses: julia-actions/setup-julia@v2
with:
version: '1.10'
- name: Load Julia packages from cache
uses: julia-actions/cache@v2
# Note: needs resolve() to fix #518
- name: Instantiate Julia environment
run: julia --project=. -e 'using Pkg; Pkg.instantiate(); Pkg.resolve()'
- name: Set up Quarto
uses: quarto-dev/quarto-actions/setup@v2
- name: Restore cached _freeze folder
id: cache-restore
uses: actions/cache/restore@v4
with:
path: |
./_freeze/
key: ${{ runner.os }}-${{ hashFiles('**/Manifest.toml') }}
- name: Render Quarto site
run: quarto render
- name: Save _freeze folder
id: cache-save
uses: actions/cache/save@v4
with:
path: |
./_freeze/
key: ${{ runner.os }}-${{ hashFiles('**/Manifest.toml') }}
- name: Deploy to GitHub Pages
uses: JamesIves/github-pages-deploy-action@v4
with:
branch: gh-pages
folder: _site
target-folder: pr-previews/${{ github.event.pull_request.number }}
clean: false
commit-message: Deploy preview for PR ${{ github.event.pull_request.number }}
token: ${{ secrets.GITHUB_TOKEN }}
comment-preview-url:
needs: build-and-preview
if: needs.build-and-preview.result == 'success'
runs-on: ubuntu-latest
steps:
- name: Comment Preview URL
uses: thollander/actions-comment-pull-request@v2
with:
message: |
<!-- preview-url-comment -->
Preview the changes: https://turinglang.org/docs/pr-previews/${{ github.event.pull_request.number }}
Please avoid using the search feature and navigation bar in PR previews!
comment_tag: preview-url-comment
env:
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
delete-preview-directory:
if: github.event.action == 'closed' || github.event.pull_request.merged == true
runs-on: ubuntu-latest
steps:
- name: Checkout gh-pages branch
uses: actions/checkout@v4
with:
ref: gh-pages
- name: Remove PR Preview Directory
run: |
PR_NUMBER=${{ github.event.pull_request.number }}
PREVIEW_DIR="pr-previews/${PR_NUMBER}"
git config --global user.name "github-actions[bot]"
git config --global user.email "github-actions[bot]@users.noreply.github.com"
git pull origin gh-pages
rm -rf ${PREVIEW_DIR}
git add .
git commit -m "Remove preview for merged PR #${PR_NUMBER}"
git push
env:
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}