Skip to content

Commit 9070441

Browse files
authored
[ fix ] preserves old HTML doc (#2) (#1517)
1 parent 0b9be77 commit 9070441

File tree

1 file changed

+8
-1
lines changed

1 file changed

+8
-1
lines changed

.github/workflows/ci-ubuntu.yml

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -84,6 +84,13 @@ jobs:
8484
cp travis/* .
8585
./index.sh
8686
${{ env.AGDA }} --safe EverythingSafe.agda
87+
${{ env.AGDA }} index.agda
88+
89+
- name: Generate HTML
90+
run: |
91+
git clone --depth 1 --single-branch --branch gh-pages https://github.com/agda/agda-stdlib html
92+
rm -f '${{ env.AGDA_HTML_DIR }}'/*.html
93+
rm -f '${{ env.AGDA_HTML_DIR }}'/*.css
8794
${{ env.AGDA }} --html --html-dir ${{ env.AGDA_HTML_DIR }} index.agda
8895
8996
# This is a massive hack at the moment
@@ -100,7 +107,7 @@ jobs:
100107
## ${{ env.AGDA }} -c README/Foreign/Haskell.agda && ./Haskell
101108

102109

103-
- name: Deploy
110+
- name: Deploy HTML
104111
uses: JamesIves/[email protected]
105112
if: ${{ success() && env.AGDA_DEPLOY }}
106113

0 commit comments

Comments
 (0)