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.