From 7b0016fc124df79d29fc7664e776648aa0b91fe1 Mon Sep 17 00:00:00 2001
From: Adam Dinwoodie <adam@dinwoodie.org>
Date: Fri, 20 Oct 2023 21:28:18 +0100
Subject: [PATCH] Separate out building user-manual.xml

Hopefully fixes #60.
---
 git.cygport | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/git.cygport b/git.cygport
index 334e363..dc9c1fc 100644
--- 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
 }