contrib/jenkins_manuals: new file

Add a separate jenkins script to build and publish the manuals. This
will use the debian-bookworm-build container, which has all dependencies
for the manuals. The other script contrib/jenkins.sh uses the
debian-bookworm-erlang container.

Related: OS#6332
Change-Id: I10f8490e37fd0e332e670b6d461997024588a00c
---
A contrib/jenkins_manuals.sh
1 file changed, 23 insertions(+), 0 deletions(-)

diff --git a/contrib/jenkins_manuals.sh b/contrib/jenkins_manuals.sh
new file mode 100755
index 0000000..3dd3d0b
--- /dev/null
+++ b/contrib/jenkins_manuals.sh
@@ -0,0 +1,8 @@
+#!/bin/sh -ex
+
+cd docs/manuals
+make
+
+if [ "$PUBLISH" = "1" ]; then
+	make publish
+fi

