# HG changeset patch
# User Paul Boddie <paul@boddie.org.uk>
# Date 1556832092 -7200
# Node ID 751c61390702984445e6bb1609b7c0aae3d0d54c
# Parent  427811b05deae7338be3ebca2d03aee7a3c7db7e
Added a documentation preparation script.

diff -r 427811b05dea -r 751c61390702 docs/tools/make_docs.sh
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/docs/tools/make_docs.sh	Thu May 02 23:21:32 2019 +0200
@@ -0,0 +1,30 @@
+#!/bin/sh
+
+THISDIR=`dirname "$0"`
+INDIR="$THISDIR/../wiki"
+OUTDIR="$THISDIR/../html"
+
+ROOT="CommonPIC32"
+
+MAPPING='--mapping WikiPedia https://en.wikipedia.org/wiki/'
+THEME='--theme mercurial'
+
+if [ "$1" = '--web' ] ; then
+    DOCINDEX=
+    shift 1
+else
+    DOCINDEX='--document-index index.html'
+fi
+
+FILENAMES=${*:-'--all'}
+
+moinconvert --input-dir "$INDIR" \
+            --input-page-sep '--' \
+            --output-dir "$OUTDIR" \
+            --root "$ROOT" \
+            --format html \
+            --macros \
+            $DOCINDEX \
+            $MAPPING \
+            $THEME \
+            $FILENAMES