Make logo link to index html #24
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
name: Deploy to pages | |
on: | |
push: | |
branches: | |
- main | |
workflow_dispatch: | |
inputs: | |
effekt_commit: | |
description: "Commit SHA of Effekt submodule to checkout and build. If omitted, the latest commit is chosen. (OPTIONAL)" | |
required: false | |
schedule: | |
- cron: '0 0 * * 2' | |
permissions: | |
contents: read | |
pages: write | |
id-token: write | |
concurrency: | |
group: "pages" | |
cancel-in-progress: false | |
jobs: | |
build: | |
runs-on: ubuntu-latest | |
steps: | |
- uses: actions/checkout@v4 | |
with: | |
submodules: 'recursive' | |
- name: Install Effekt dependencies | |
uses: effekt-lang/effekt/.github/actions/setup-effekt@master | |
- name: Install other dependencies | |
run: sudo apt-get install jq gzip | |
- name: Checkout given commit | |
if: "${{ github.event.inputs.effekt_commit != '' }}" | |
run: | | |
git -C effekt/ fetch --all | |
git -C effekt/ checkout ${{ github.event.inputs.effekt_commit }} | |
- name: Checkout most recent commit | |
if: "${{ github.event.inputs.effekt_commit == '' }}" | |
run: | | |
git -C effekt/ checkout master | |
git -C effekt/ pull | |
- name: Install Effekt | |
run: cd effekt/ && sbt install | |
- name: Generate documentation | |
run: ./gen.sh html | |
- name: Set up pages | |
id: pages | |
uses: actions/configure-pages@v5 | |
- name: Upload artifact | |
uses: actions/upload-pages-artifact@v3 | |
with: | |
path: build/ | |
deploy: | |
environment: | |
name: github-pages | |
url: ${{ steps.deployment.outputs.page_url }} | |
runs-on: ubuntu-latest | |
needs: build | |
steps: | |
- name: Deploy to GitHub Pages | |
id: deployment | |
uses: actions/deploy-pages@v4 |