From 357995a15a0c33edfb5b42af900a168169600a1c Mon Sep 17 00:00:00 2001
From: John Maximilian <2e0byo@gmail.com>
Date: Wed, 8 Mar 2023 11:41:58 +0000
Subject: [PATCH] ci: add index.html.
Currently this is just a redirect, but we could build for different versions and
add a menu.
---
.github/static-files/index.html | 8 ++++++++
.github/workflows/docs.yaml | 3 +--
2 files changed, 9 insertions(+), 2 deletions(-)
create mode 100644 .github/static-files/index.html
diff --git a/.github/static-files/index.html b/.github/static-files/index.html
new file mode 100644
index 0000000..f175c8c
--- /dev/null
+++ b/.github/static-files/index.html
@@ -0,0 +1,8 @@
+
+
+
+
+
+ Please click here if you are not automatically redirected.
+
+
diff --git a/.github/workflows/docs.yaml b/.github/workflows/docs.yaml
index a5e9d5b..93fe658 100644
--- a/.github/workflows/docs.yaml
+++ b/.github/workflows/docs.yaml
@@ -31,6 +31,7 @@ jobs:
- name: build docs
run: |
cargo doc --no-deps
+ cp .github/static-files/index.html target/doc/
- name: Upload artifact
uses: actions/upload-pages-artifact@v1
with:
@@ -43,8 +44,6 @@ jobs:
url: ${{ steps.deployment.outputs.page_url }}
runs-on: ubuntu-latest
steps:
- - name: Checkout
- uses: actions/checkout@v3
- name: Setup Pages
uses: actions/configure-pages@v3
- name: Deploy to GitHub Pages