-
Notifications
You must be signed in to change notification settings - Fork 1
49 lines (41 loc) · 1.5 KB
/
deploy.yml
File metadata and controls
49 lines (41 loc) · 1.5 KB
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
name: deploy
on:
push:
branches:
- main
jobs:
deploy:
runs-on: ubuntu-latest
container:
image: nixos/nix:latest
steps:
- name: deploy
run: |
set -x
git clone https://github.com/${{ github.repository }}.git
cd $(basename ${{ github.repository }})
echo "github.event_name is ${{ github.event_name }}"
# fetch the current PR/branch
if [ "${{ github.event_name }}" = "pull_request" ]; then
echo "Fetching PR branch"
git fetch origin pull/${{ github.event.pull_request.number }}/head:pr-${{ github.event.pull_request.number }}
git checkout pr-${{ github.event.pull_request.number }}
else
echo "Fetching current branch"
git checkout ${{ github.ref_name }}
fi
nix-shell --run "
dune build @doc &&
mv _build/default/_doc/_html doc
"
touch doc/.nojekyll
git config --global user.name "github-actions[bot]"
git config --global user.email "github-actions[bot]@users.noreply.github.com"
git clone https://x-access-token:${{ secrets.GITHUB_TOKEN }}@github.com/${{ github.repository }} gh-pages
cd gh-pages
git checkout gh-pages || git checkout --orphan gh-pages
rm -rf ./*
cp -r ../doc/* ./
git add .
git commit -m "Deploy docs from ${GITHUB_SHA}" || echo "No changes to commit"
git push origin gh-pages