Separate out building user-manual.xml

Hopefully fixes #60.
cygporter · Oct 20, 2023 · 7b0016f · 7b0016f
1 parent 89f1af2
commit 7b0016f
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/git.cygport b/git.cygport
@@ -91,6 +91,11 @@ src_compile() {
 	lndirs
 	cd ${B}
 	cygconf --with-libpcre
+
+	# Make the user manual XML file separately, in an attempt to avoid an
+	# apparent race condition I see intermittently.
+	( cd "${B}/Documentation" && cygmake user-manual.xml )
+
 	cygmake all html man info pdf
 }