Skip to content

Update to Pluto 0.19.26 #512

Update to Pluto 0.19.26

Update to Pluto 0.19.26 #512

Workflow file for this run

name: Docs
on:
push:
branches:
- main
tags: '*'
pull_request:
workflow_dispatch:
jobs:
BuildAndDeploy:
name: Documentation
runs-on: ubuntu-latest
timeout-minutes: 20
steps:
- uses: actions/checkout@v2
- uses: julia-actions/julia-buildpkg@latest
- uses: julia-actions/julia-docdeploy@latest
if: ${{ github.event_name != 'pull_request' }}
env:
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
DOCUMENTER_KEY: ${{ secrets.DOCUMENTER_KEY }}
MonoDeploy:
needs: BuildAndDeploy
runs-on: ubuntu-latest
if: ${{ github.event_name != 'pull_request' }}
steps:
- name: Clone `docs-output` branch
uses: actions/checkout@v2
with:
ref: 'docs-output'
- uses: webfactory/ssh-agent@v0.5.4
with:
ssh-private-key: ${{ secrets.DEPLOY_KEY }}
# Fixes CloudFlare Pages not redirecting `stable/`
# Also, this makes documentation fixes visible without releasing a new version.
- name: Default to `dev`
shell: julia --color=yes {0}
run: |
filename = "index.html"
if isfile(filename)
run(`sed --debug -i 's/stable/dev/g' $filename`)
end
- name: Deploy to https://huijzer.xyz/PlutoStaticHTML.jl
shell: julia --color=yes {0}
run: |
function generate_redirects(dir)
cd(dir) do
redirects = String[]
for (root, _, files) in walkdir(".")
for file in files
path = joinpath(root, file)
if islink(path)
url_root = lstrip(root, '.')
from = joinpath(url_root, file)
# End with forward slashes to get redirects to index.html
to = joinpath(url_root, readlink(path) * '/')
redirect = "$from $to 301"
@info redirect
push!(redirects, redirect)
end
end
end
text = join(redirects, '\n')
write("_redirects", text)
return nothing
end
end
from = "."
clone = mktempdir()
url = "git@github.com:rikhuijzer/huijzer.xyz.git"
run(`git clone --depth=1 $url $clone`)
to = joinpath(clone, "public", "PlutoStaticHTML.jl")
mkpath(to)
cp(from, to; force=true)
# To avoid Git submodules.
rm(joinpath(to, ".git"); recursive=true)
generate_redirects(joinpath(clone, "public"))
cd(clone) do
run(`git add .`)
run(`git config --global user.email 't.h.huijzer@rug.nl'`)
run(`git config --global user.name 'Bot'`)
run(`git commit --allow-empty -m 'Deploy from PlutoStaticHTML.jl'`)
run(`git push`)
end