Fix build scripts for manpages

tdgroot · tdgroot · commit c659dba1654a · 2025-08-19T12:21:27.000+02:00
The documentation name has been changed from docs to documentation
recently, so has the resulting name of the manpage file.
diff --git a/bin/build_manpage b/bin/build_manpage
@@ -4,5 +4,5 @@ set -e
 
 pushd docs
 make man
-echo "manpage located at $(realpath _build/man/docs.1)"
+echo "manpage located at $(realpath _build/man/documentation.1)"
 popd
diff --git a/debian/rules b/debian/rules
@@ -10,7 +10,7 @@ build:
 	venv/bin/pip install wheel
 	venv/bin/pip install -r requirements/development.txt
 	bash -c 'source venv/bin/activate; bin/build_manpage'
-	mv docs/_build/man/docs.1 docs/_build/man/hypernode.3
+	mv docs/_build/man/documentation.1 docs/_build/man/hypernode.3
 
 override_dh_usrlocal:
 
