Install docs

1 files changed, 3 insertions, 0 deletions

diff --git a/build b/build
index 74c7d9b..13160ea 100755
--- a/build
+++ b/build
@@ -125,6 +125,9 @@ main() {
     genrss index news index.html > src/news.xml
     genrss src/blog > src/rss.xml
 
+    # Generate htmldocs
+    make -s -C texidocs DESTDIR="$PWD/src/docs" htmldocs
+
     # Generate pages
     genpages
 }