From e85f8eea9dfe76dacc86728b20c4a0036ec71c1d Mon Sep 17 00:00:00 2001
From: LMBishop <13875753+LMBishop@users.noreply.github.com>
Date: Wed, 5 Jul 2023 15:28:17 +0100
Subject: Add /docs directory

This is part of a migration from GitHub wikis to GitHub pages
---
 docs/_scripts/convert-mediawiki-to-markdown.sh | 10 ++++++++++
 1 file changed, 10 insertions(+)
 create mode 100755 docs/_scripts/convert-mediawiki-to-markdown.sh

(limited to 'docs/_scripts')

diff --git a/docs/_scripts/convert-mediawiki-to-markdown.sh b/docs/_scripts/convert-mediawiki-to-markdown.sh
new file mode 100755
index 00000000..25f9afd4
--- /dev/null
+++ b/docs/_scripts/convert-mediawiki-to-markdown.sh
@@ -0,0 +1,10 @@
+#!/bin/bash
+
+# This script converts mediawiki formatted files in the current
+# working directory to markdown using pandoc.
+
+for FILE in *.mediawiki; do
+    echo "Processing $FILE"
+    FILENAME=$(basename $FILE .mediawiki)
+    sed ':a; N; $!ba; s/```yaml\([^`]*\)```/<syntaxhighlight lang="yaml">\1<\/syntaxhighlight>/g; s/```\([^`]*\)```/<syntaxhighlight>\1<\/syntaxhighlight>/g' $FILE | pandoc -f mediawiki -t gfm -o "$FILENAME.md"
+done
-- 
cgit v1.2.3-70-g09d2