diff options
Diffstat (limited to 'pkgs/data/documentation/rnrs/builder.sh')
| -rw-r--r-- | pkgs/data/documentation/rnrs/builder.sh | 12 |
1 files changed, 0 insertions, 12 deletions
diff --git a/pkgs/data/documentation/rnrs/builder.sh b/pkgs/data/documentation/rnrs/builder.sh deleted file mode 100644 index 6ec5c855ababe..0000000000000 --- a/pkgs/data/documentation/rnrs/builder.sh +++ /dev/null @@ -1,12 +0,0 @@ -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'" - -mkdir -p "$out/share/info" && \ -makeinfo -o "$out/share/info/${reportName}.info" "$src" - -# XXX: HTML output is apparently broken. -#mkdir -p "$out/share/doc/${reportName}" && \ -#makeinfo -o "$out/share/doc/${reportName}/html" --html --force "$src" |