2022-06-30 20:34:29 +02:00
|
|
|
#!/bin/sh
|
|
|
|
|
|
|
|
infodir=$1
|
|
|
|
infofile=$2
|
|
|
|
|
|
|
|
# Meson post-install script to update info metadata
|
2023-09-03 16:33:08 +02:00
|
|
|
|
2022-07-05 23:56:48 +02:00
|
|
|
# If DESTDIR is set, do _not_ install-info, since it's only a temporary
|
|
|
|
# install
|
|
|
|
if test -z "${DESTDIR}"; then
|
2023-09-03 16:33:08 +02:00
|
|
|
install-info --info-dir "${infodir}" "${infodir}/${infofile}"
|
2023-11-03 22:02:42 +01:00
|
|
|
gzip --best --force "${infodir}/${infofile}"
|
2022-07-05 23:56:48 +02:00
|
|
|
fi
|