2008-03-27 15:40:08 +01:00
|
|
|
source "$stdenv/setup" || exit 1
|
|
|
|
|
|
|
|
# XXX: Eventually we could consider building the PDF/PS files as well.
|
|
|
|
|
|
|
|
echo "source is \`$src', report name is \`$reportName'"
|
|
|
|
|
2012-01-18 21:16:00 +01:00
|
|
|
mkdir -p "$out/share/info" && \
|
2008-03-27 15:40:08 +01:00
|
|
|
makeinfo -o "$out/share/info/${reportName}.info" "$src"
|
|
|
|
|
|
|
|
# XXX: HTML output is apparently broken.
|
2012-01-18 21:16:00 +01:00
|
|
|
#mkdir -p "$out/share/doc/${reportName}" && \
|
2008-03-27 15:40:08 +01:00
|
|
|
#makeinfo -o "$out/share/doc/${reportName}/html" --html --force "$src"
|