Skip to content

Commit 222c238

Browse files
gallaisjamesmckinna
gallais
authored and
jamesmckinna
committed
[ fix agda#2086 ] new web deployment strategy (agda#2147)
1 parent 6e375c2 commit 222c238

File tree

5 files changed

+66
-1
lines changed

5 files changed

+66
-1
lines changed

‎.github/workflows/ci-ubuntu.yml

+5-1
Original file line numberDiff line numberDiff line change
@@ -75,7 +75,7 @@ jobs:
7575
|| '${{ github.base_ref }}' == 'master' ]]; then
7676
# Pick Agda version for master
7777
echo "AGDA_COMMIT=tags/v2.6.4" >> $GITHUB_ENV;
78-
echo "AGDA_HTML_DIR=html" >> $GITHUB_ENV
78+
echo "AGDA_HTML_DIR=html/master" >> $GITHUB_ENV
7979
elif [[ '${{ github.ref }}' == 'refs/heads/experimental' \
8080
|| '${{ github.base_ref }}' == 'experimental' ]]; then
8181
# Pick Agda version for experimental
@@ -125,6 +125,7 @@ jobs:
125125
run: cabal update
126126

127127
- name: Install alex & happy
128+
if: steps.cache-cabal.outputs.cache-hit != 'true'
128129
run: |
129130
${{ env.CABAL_INSTALL }} alex
130131
${{ env.CABAL_INSTALL }} happy
@@ -177,6 +178,9 @@ jobs:
177178
rm -f '${{ env.AGDA_HTML_DIR }}'/*.css
178179
${{ env.AGDA }} --html --html-dir ${{ env.AGDA_HTML_DIR }} index.agda
179180
181+
cp travis/* .
182+
./landing.sh
183+
180184
- name: Deploy HTML
181185
uses: JamesIves/[email protected]
182186
if: ${{ success() && env.AGDA_DEPLOY }}

‎travis/agda-logo.svg

+16
Loading

‎travis/landing-bottom.html

+4
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
</ul>
2+
</div>
3+
</body>
4+
</html>

‎travis/landing-top.html

+24
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
<html>
2+
3+
<head>
4+
<title>Documention for the Agda standard library</title>
5+
</head>
6+
7+
<body>
8+
9+
<div id="container" style="width:50%;min-width:500px;margin:auto">
10+
<img src="agda-logo.svg" style="width:80px;float:right" />
11+
<h1>Documention for the Agda standard library</h1>
12+
13+
<hr />
14+
15+
<h2>Development versions</h2>
16+
17+
<ul>
18+
<li><a href="master">master</a></li>
19+
<li><a href="experimental">experimental</a></li>
20+
</ul>
21+
22+
<h2>Released versions</h2>
23+
24+
<ul>

‎travis/landing.sh

+17
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
set -eu
2+
set -o pipefail
3+
4+
rm html/index.html
5+
6+
cat landing-top.html >> landing.html
7+
8+
find html/ -name "index.html" \
9+
| grep -v "master\|experimental" \
10+
| sort -r \
11+
| sed 's|html/\([^\/]*\)/index.html| <li><a href="\1">\1</a></li>|g' \
12+
>> landing.html
13+
14+
cat landing-bottom.html >> landing.html
15+
16+
mv landing.html html/index.html
17+
mv agda-logo.svg html/

0 commit comments

Comments
 (0)