1 | # Common functions for soil/
|
2 |
|
3 | # Include guard.
|
4 | test -n "${__SOIL_COMMON_SH:-}" && return
|
5 | readonly __SOIL_COMMON_SH=1
|
6 |
|
7 | log() {
|
8 | echo "$@" 1>&2
|
9 | }
|
10 |
|
11 | log-context() {
|
12 | local label=$1
|
13 |
|
14 | log ''
|
15 | log "$label: running as user '$(whoami)' on host '$(hostname)' in dir $PWD"
|
16 | log ''
|
17 | }
|
18 |
|
19 | dump-env() {
|
20 | env | grep -v '^encrypted_' | sort
|
21 | }
|
22 |
|
23 | if false; then
|
24 | readonly SOIL_USER='travis_admin'
|
25 | readonly SOIL_HOST='travis-ci.oilshell.org'
|
26 | readonly SOIL_HOST_DIR=~/travis-ci.oilshell.org # used on server
|
27 | readonly SOIL_REMOTE_DIR=travis-ci.oilshell.org # used on client
|
28 | elif false; then
|
29 | readonly SOIL_USER='oils'
|
30 | readonly SOIL_HOST='mb.oils.pub'
|
31 | # Extra level
|
32 | readonly SOIL_HOST_DIR=~/www/mb.oils.pub # used on server
|
33 | readonly SOIL_REMOTE_DIR=www/mb.oils.pub # used on client
|
34 | else
|
35 | readonly SOIL_USER='oils'
|
36 | readonly SOIL_HOST='op.oils.pub'
|
37 | readonly SOIL_HOST_DIR=~/op.oils.pub # used on server
|
38 | readonly SOIL_REMOTE_DIR=op.oils.pub # used on client
|
39 | fi
|
40 |
|
41 | readonly SOIL_USER_HOST="$SOIL_USER@$SOIL_HOST"
|
42 |
|
43 | html-head() {
|
44 | # TODO: Shebang line should change too
|
45 | PYTHONPATH=. python3 doctools/html_head.py "$@"
|
46 | }
|
47 |
|
48 | # NOTE: soil-html-head and table-sort-html-head are distinct, because they
|
49 | # collide with <td> styling and so forth
|
50 |
|
51 | soil-html-head() {
|
52 | local title="$1"
|
53 | local web_base_url=${2:-'/web'}
|
54 |
|
55 | html-head --title "$title" \
|
56 | "$web_base_url/base.css?cache=0" "$web_base_url/soil.css?cache=0"
|
57 | }
|
58 |
|
59 | table-sort-html-head() {
|
60 | local title="$1"
|
61 | local web_base_url=${2:-'/web'}
|
62 |
|
63 | html-head --title "$title" \
|
64 | "$web_base_url/base.css?cache=0" \
|
65 | "$web_base_url/ajax.js?cache=0" \
|
66 | "$web_base_url/table/table-sort.css?cache=0" "$web_base_url/table/table-sort.js?cache=0"
|
67 | }
|
68 |
|
69 | git-commit-dir() {
|
70 | local prefix=$1
|
71 |
|
72 | # written by save-metadata in soil/worker.sh
|
73 | local commit_hash
|
74 | commit_hash=$(cat _tmp/soil/commit-hash.txt)
|
75 |
|
76 | local git_commit_dir="$SOIL_REMOTE_DIR/${prefix}jobs/git-$commit_hash"
|
77 |
|
78 | echo $git_commit_dir
|
79 | }
|
80 |
|
81 | git-commit-url() {
|
82 | local prefix=$1
|
83 |
|
84 | # written by save-metadata in soil/worker.sh
|
85 | local commit_hash
|
86 | commit_hash=$(cat _tmp/soil/commit-hash.txt)
|
87 |
|
88 | # https:// not working on Github Actions?
|
89 | local url="http://$SOIL_HOST/${prefix}jobs/git-$commit_hash"
|
90 |
|
91 | echo $url
|
92 | }
|