aboutsummaryrefslogtreecommitdiff
path: root/build
diff options
context:
space:
mode:
Diffstat (limited to 'build')
-rwxr-xr-xbuild5
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