File tree 3 files changed +45
-12
lines changed
3 files changed +45
-12
lines changed Original file line number Diff line number Diff line change
1
+ # EditorConfig helps maintain consistent coding styles for multiple developers working on the same project across various editors and IDEs.
2
+ # More: https://editorconfig.org/
3
+
4
+ root = true
5
+
6
+ [* ]
7
+ indent_style = space
8
+ indent_size = 2
9
+ trim_trailing_whitespace = true
10
+ insert_final_newline = true
11
+ charset = utf-8
12
+ end_of_line = lf
13
+
14
+ [Makefile ]
15
+ indent_style = tab
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
+ git_branch=$( git rev-parse --abbrev-ref HEAD)
8
+
9
+ git config user.name github-actions
10
+ git config user.email github-actions@github.com
11
+
12
+ stack exec --system-ghc site rebuild
13
+
14
+ site_src=" ${git_repo_root} /_site"
15
+ site_dest=" ${git_repo_root} /branches/${git_branch} "
16
+
17
+ git checkout gh-pages
18
+ git pull --rebase
19
+
20
+ # Overwrite existing files with new files
21
+ rm -rf " ${site_dest} "
22
+ mkdir -p " ${site_dest} "
23
+ cp -a -v " ${site_src} " " ${site_dest} "
24
+
25
+ # Commit
26
+ git add --all
27
+ git commit -m " [$( date ' +%F %T %Z' ) ] Updated site for the '${git_branch} ' branch [ci skip]"
28
+ # Push
29
+ git push origin gh-pages
Original file line number Diff line number Diff line change 54
54
# Runs a set of commands using the runners shell
55
55
- name : Deploy
56
56
run : |
57
- git config user.name github-actions
58
- git config user.email github-actions@github.com
59
- stack exec --system-ghc site rebuild
60
- git checkout main
61
- git pull --rebase
62
- # Overwrite existing files with new files
63
- cp -a -v _site/. .
64
- # Commit
65
- git add --all
66
- git commit -m "[`date '+%F %T %Z'`] New release [ci skip]"
67
- # Push
68
- git push origin main:main
57
+
You can’t perform that action at this time.
0 commit comments