From e539bde6508ed58e2bbe046a9c1720fe9cf501d5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=C3=81rni=20Dagur?= <agudmundsson@fc-md.umd.edu>
Date: Sun, 24 May 2020 02:57:26 -0400
Subject: Place a 'index.html' file at the root of Github Pages

---
 web/create_site.bash | 10 ++++++++++
 1 file changed, 10 insertions(+)
 create mode 100644 web/create_site.bash

(limited to 'web/create_site.bash')

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
-- 
cgit v1.2.3