6161 cd coverage_repository
6262 }
6363
64- add_event() {
65- (
66- if ! grep -q "$GITHUB_EVENT_NAME" index.html; then
67- perl -pi -e 's#^(\s+)(</ul>)#$1 <li><a href="$ENV{GITHUB_EVENT_NAME}/">$ENV{GITHUB_EVENT_NAME}</a></li>\n$1$2#' index.html
68- git add index.html
69- git \
70- -c user.email="$user_email" \
71- -c user.name="$user_name" \
72- commit -m "Add $GITHUB_EVENT_NAME listing"
73- fi
74- )
75- }
76-
77- add_event_list() {
78- (
79- if [ ! -e index.html ]; then
80- printf "<html><head><title>check-spelling coverage for $GITHUB_EVENT_NAME</title></head>\n<body>\n <h1>check-spelling coverage for $GITHUB_EVENT_NAME</h1>\n <ul>\n </ul>\n</body></html>\n" > index.html
81- git add index.html
82- git \
83- -c user.email="$user_email" \
84- -c user.name="$user_name" \
85- commit -m "Add $GITHUB_EVENT_NAME list"
86- fi
87- )
88- }
89-
90- add_event_listing() {
91- (
92- cd "$GITHUB_EVENT_NAME"
93- add_event_list
94- if ! grep -q "$sha" index.html; then
95- date="$date" \
96- perl -pi -e 's#^(\s*)(<ul>)#$1$2\n$1 <li><a href="$ENV{sha}/">$ENV{date} ($ENV{sha})</a></li>#' index.html
97- git add index.html
98- git \
99- -c user.email="$user_email" \
100- -c user.name="$user_name" \
101- commit -m "Add $GITHUB_EVENT_NAME listing for $sha"
102- fi
103- )
104- }
105-
10664 add_coverage() {
10765 (
66+ git switch --orphan="ref-$GITHUB_EVENT_NAME-$sha"
10867 mkdir -p "$GITHUB_EVENT_NAME/$sha"
10968 cd "$GITHUB_EVENT_NAME/$sha"
11069
@@ -125,42 +84,6 @@ runs:
12584 )
12685 }
12786
128- add_everything() {
129- add_coverage
130- add_event_listing
131- add_event
132- }
133-
134- try_push() {
135- git push origin HEAD
136- }
137-
138- try_publish_or_rebase() {
139- add_everything
140- if try_push; then
141- return
142- fi
143- if git pull --rebase origin; then
144- if try_push; then
145- return
146- fi
147- fi
148- while [ -e .git/rebase-merge/git-rebase-todo ]; do
149- git clean
150- git rebase --skip
151- done
152- false
153- }
154-
155- try_publish_with_retries() {
156- for attempt in $(seq 3); do
157- if try_publish_or_rebase; then
158- return
159- fi
160- false
161- done
162- }
163-
16487 report_coverage_published_pending() {
16588 if [ -z "$github_pages_base" ]; then
16689 github_pages_base="https://${coverage_repository%%/*}.github.io/${coverage_repository##*/}"
@@ -181,7 +104,8 @@ runs:
181104 }
182105
183106 configure_environment
184- if try_publish_with_retries; then
107+ add_coverage
108+ if git push origin HEAD; then
185109 report_coverage_published_pending
186110 else
187111 report_coverage_published_failed
0 commit comments