diff options
Diffstat (limited to 'render_locally')
-rwxr-xr-x | render_locally | 55 |
1 files changed, 29 insertions, 26 deletions
diff --git a/render_locally b/render_locally index e1c27748..29ab828b 100755 --- a/render_locally +++ b/render_locally @@ -1,36 +1,39 @@ #!/bin/sh -# Render the pages of this repository for your local browsing pleasure. - -# We use ``--no-usedirs'' here, because when browsing local files, the web -# browsers don't display `index.html' files by default when a hyperlink -# referencing a directory is being opened. +# Render the pages of this repository. # Written by Thomas Schwinge <tschwinge@gnu.org> +export ROOT && ROOT=$(readlink -f "$(dirname "$0")") && -# Need a symlink-free path. -src=$(readlink -f "$(dirname "$0")") && -dest=$src.rendered && +case $1 in + --official) + # Use this for rendering the set of pages which are to be installed under + # <http://www.gnu.org/software/hurd/>. Use ``--no-usedirs'' here, so that + # not too many separate directories have to be created. + shift && + export TZ && TZ=UTC && + export DESTDIR && DESTDIR=$ROOT.rendered.official && + set x \ + --set wikistatedir="$ROOT"/.ikiwiki-official \ + --url http://www.gnu.org/software/hurd \ + --no-usedirs \ + "$@" && + shift;; + *) + # Use ``--no-usedirs'' here, because when browsing local files, the web + # browsers don't display `index.html' files by default when a hyperlink + # referencing a directory is being opened. + set x \ + --no-usedirs \ + "$@" && + shift;; +esac && ikiwiki \ - --verbose \ - --wikiname GNU\ Hurd \ - --templatedir "$src"/.templates \ - --userdir user \ - --no-usedirs \ - --plugin favicon \ - --plugin goodstuff \ - --plugin html \ - --plugin sidebar \ - --plugin table \ - --plugin txt \ - --libdir "$src"/.library \ - --plugin copyright \ - --plugin license \ - --plugin texinfo \ - ${1+"$@"} \ - "$src" "$dest" && + --setup "$ROOT"/ikiwiki.setup \ + --refresh \ + "$@" && echo && -echo Now\ open\ \`"$dest"/index.html\'' to browse the web pages.' +echo Now\ open\ \`"${DESTDIR-"$ROOT".rendered}"/index.html\'' to browse the web pages.' |