1 files changed, 4 insertions, 1 deletions
diff --git a/build b/build
index 13160ea..9e78fa8 100755
--- a/build
+++ b/build
@@ -126,7 +126,10 @@ main() {
     genrss src/blog > src/rss.xml
 
     # Generate htmldocs
-    make -s -C texidocs DESTDIR="$PWD/src/docs" htmldocs
+    command -v makeinfo && {
+        git submodule update --init --remote -f
+        make -s -C texidocs DESTDIR="$PWD/src/docs" htmldocs
+    }
 
     # Generate pages
     genpages