From c659dba1654acd2b0eabecfadda5368079905d46 Mon Sep 17 00:00:00 2001 From: Timon de Groot Date: Tue, 19 Aug 2025 12:21:27 +0200 Subject: [PATCH] Fix build scripts for manpages The documentation name has been changed from docs to documentation recently, so has the resulting name of the manpage file. --- bin/build_manpage | 2 +- debian/rules | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/bin/build_manpage b/bin/build_manpage index e8a8689c..5e774d15 100755 --- 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 index fb0201ed..3d5a9ea4 100755 --- 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: