Place a 'index.html' file at the root of Github Pages

1 files changed, 10 insertions, 0 deletions

diff --git a/web/create_site.bash b/web/create_site.bash
new file mode 100644
index 0000000..b106d8c
--- /dev/null
+++ b/web/create_site.bash
@@ -0,0 +1,10 @@
+#!/bin/bash
+set -euxo pipefail
+
+# This script assumes that the current working directory is the repository
+# root.
+
+mkdir -p target
+cp -r web/static target/github-pages
+cargo doc --all-features
+cp -r target/doc target/github-pages/docs