A shell script to ``render the pages of this repository for your local browsing pleasure.''

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.'