Rebuild docs

aionescu · Jan 18, 2024 · 142643b · 142643b
1 parent f6a44ed
commit 142643b
Show file tree

Hide file tree

Showing 5 changed files with 7 additions and 12 deletions.
diff --git a/.gitignore b/.gitignore
@@ -1,7 +1 @@
-_build/
-*/.merlin
-*.cmi
-*.cmx
-*.o
-*.out
-.vscode/
+_build
diff --git a/copy-docs.sh → build-docs.sh b/copy-docs.sh → build-docs.sh
@@ -1,3 +1,6 @@
 #!/bin/sh
+set -eu
+
+dune build @doc
 rm -rf docs/docs
 cp -a _build/default/_doc/_html/. docs/docs