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
+ git_repo_root=$( git rev-parse --show-toplevel)
6
+
7
+ # replace "/", "#", etc with "-".
8
+ slugify () {
9
+ 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
10
+ }
11
+ git_branch=$( slugify $( git rev-parse --abbrev-ref HEAD) )
12
+ echo " Current git branch is '${git_branch} '"
13
+
14
+ git config user.name github-actions
15
+ git config user.email
[email protected]
16
+
17
+ stack build --system-ghc
18
+ stack exec --system-ghc site build
19
+
20
+ site_src=" ${git_repo_root} /_site"
21
+ site_dest=" ${git_repo_root} /branches/${git_branch} "
22
+
23
+ git checkout gh-pages
24
+ git pull origin gh-pages
25
+
26
+ # Overwrite existing files with new files
27
+ rm -rf " ${site_dest} "
28
+ mkdir -p " ${site_dest} "
29
+ cp -a -v ${site_src} /* " ${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