Generated docs get copied to docs folder

mcneissue · Oct 19, 2020 · 5f17c15 · 5f17c15
1 parent 5f9b460
commit 5f17c15
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 1 deletion.
diff --git a/.gitignore b/.gitignore
@@ -10,4 +10,5 @@
 /.spago
 /.cache
 /bundle/
-/dist
+/dist
+/docs
diff --git 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.
-Original file line number
+Diff line change
@@ Expand Up / @@ -10,4 +10,5 @@ @@
     /.spago
     /.cache
     /bundle/
-    /dist
+    /dist
+    /docs