doc: install the HTML manual again

In 0e6b3435a1, installation of the HTML manual
was accidentally dropped: setting install_dir on a custom_target only sets the
directory where something is going to be installed if it is installed at all,
but does not itself trigger installation. The latter has to be explicitly
requested, which is just what we do here to get the manual back.

Change-Id: Iff8b791de7e7cb4c8d747c2a9b1154b5fcc32fe0
This commit is contained in:
alois31 2024-10-05 10:49:34 +02:00
parent 5b1715e633
commit 5df2cccc49
Signed by untrusted user: alois31
GPG key ID: E0F59EA5E5216914

View file

@ -126,6 +126,7 @@ manual = custom_target(
'manual',
'markdown',
],
install : true,
install_dir : [
datadir / 'doc/nix',
false,