diff options
| -rwxr-xr-x | render_locally | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/render_locally b/render_locally new file mode 100755 index 00000000..47146656 --- /dev/null +++ b/render_locally @@ -0,0 +1,28 @@ +#!/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. + +# Written by Thomas Schwinge <tschwinge@gnu.org> + + +src=$(dirname "$0") && +# Invoking ikiwiki with ``src=.'' will make it render `.git/' as well. +if [ "$src" = . ] +then src=$(pwd) +else : +fi && +dest=$src.rendered && + +ikiwiki \ + --verbose \ + --wikiname GNU\ Hurd\ wiki \ + --userdir user \ + --no-usedirs \ + "$src" "$dest" && + +echo && +echo Now\ open\ \`"$dest"/index.html\'' to browse the wiki pages.' |