-
Notifications
You must be signed in to change notification settings - Fork 12
69 lines (57 loc) · 2.11 KB
/
pages.yml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
# This is a basic workflow to help you get started with Actions
name: CI
# Controls when the workflow will run
on:
# Triggers the workflow on push or pull request events but only for the "master" branch
push:
branches: [ "master" ]
pull_request:
branches: [ "master" ]
# Allows you to run this workflow manually from the Actions tab
workflow_dispatch:
# A workflow run is made up of one or more jobs that can run sequentially or in parallel
jobs:
# This workflow contains a single job called "build"
build:
# The type of runner that the job will run on
runs-on: ubuntu-22.04
# Steps represent a sequence of tasks that will be executed as part of the job
steps:
# Checks-out your repository under $GITHUB_WORKSPACE, so your job can access it
- uses: actions/checkout@v3
# Convert .tex to .pdf
- uses: xu-cheng/latex-action@v3
with:
root_file: "**/*.tex"
glob_root_file: true
work_in_root_file_dir: true
extra_system_packages: "inkscape" # Inkscape for SVGs
latexmk_shell_escape: true
# Runs a set of commands using the runners shell
- name: Run buildscript
run: ./build.sh build
- name: Upload GitHub Pages artifact
uses: actions/[email protected]
with:
# Artifact name
path: .
# Duration after which artifact will expire in days.
deploy:
# Only run on the master branch (not on PRs)
if: github.ref == 'refs/heads/master'
# Add a dependency to the build job
needs: build
# Grant GITHUB_TOKEN the permissions required to make a Pages deployment
permissions:
pages: write # to deploy to Pages
id-token: write # to verify the deployment originates from an appropriate source
# Deploy to the github-pages environment
environment:
name: github-pages
url: ${{ steps.deployment.outputs.page_url }}
# Specify runner + deployment step
runs-on: ubuntu-22.04
steps:
- name: Deploy to GitHub Pages
id: deployment
uses: actions/deploy-pages@v4