File tree 1 file changed +36
-0
lines changed
1 file changed +36
-0
lines changed Original file line number Diff line number Diff line change
1
+ #! /usr/bin/env bash
2
+
3
+ set -exo pipefail
4
+
5
+ script_dir=$( dirname " $0 " )
6
+ git_repo_root=$( git rev-parse --show-toplevel)
7
+
8
+ # replace "/", "#", etc with "-".
9
+ slugify () {
10
+ echo " $1 " | iconv -c -t ascii//TRANSLIT | sed -E ' s/[~^]+/-/g' | sed -E ' s/[^a-zA-Z0-9]+/-/g' | sed -E ' s/^-+|-+$/-/g' | tr A-Z a-z
11
+ }
12
+ git_branch=$( slugify $( git rev-parse --abbrev-ref HEAD) )
13
+ echo " Current git branch is ${git_branch} "
14
+
15
+ git config user.name github-actions
16
+ git config user.email github-actions@github.com
17
+
18
+ stack build --system-ghc
19
+ stack exec --system-ghc site build
20
+
21
+ site_src=" ${git_repo_root} /_site"
22
+ site_dest=" ${git_repo_root} /branches/${git_branch} "
23
+
24
+ git checkout gh-pages
25
+ git pull origin gh-pages
26
+
27
+ # Overwrite existing files with new files
28
+ rm -rf " ${site_dest} "
29
+ mkdir -p " ${site_dest} "
30
+ cp -a -v " ${site_src} " " ${site_dest} "
31
+
32
+ git add --all
33
+ git commit --allow-empty -m " [$( date ' +%F %T %Z' ) ] Updated site for the '${git_branch} ' branch [ci skip]"
34
+ git push --force origin gh-pages
35
+
36
+ echo " Deployment finished"
You can’t perform that action at this time.
0 commit comments