From 5f17c155cc97f6da5c2456f9d9f2e1b4f89c529a Mon Sep 17 00:00:00 2001
From: "John C. Lavelle" <jlavelle604@gmail.com>
Date: Sun, 18 Oct 2020 21:00:08 -0400
Subject: [PATCH] Generated docs get copied to docs folder

---
 .gitignore          | 3 ++-
 scripts/mkDocs.fish | 5 +++++
 2 files changed, 7 insertions(+), 1 deletion(-)

diff --git a/.gitignore b/.gitignore
index dc75f77..46150f0 100644
--- a/.gitignore
+++ b/.gitignore
@@ -10,4 +10,5 @@
 /.spago
 /.cache
 /bundle/
-/dist
\ No newline at end of file
+/dist
+/docs
diff --git a/scripts/mkDocs.fish b/scripts/mkDocs.fish
index 367ce7e..b9efd40 100644
--- a/scripts/mkDocs.fish
+++ b/scripts/mkDocs.fish
@@ -1,3 +1,8 @@
 set root (realpath (dirname (status --current-filename)))/..
+echo Deleting old documentation in $root/docs
+rm -rf $root/docs
 cd $root/examples
 spago docs
+echo Copying generated documentation to $root/docs
+rsync -a $root/examples/generated-docs/html/ $root/docs/
+echo Done.