Add /docs directory

This is part of a migration from GitHub wikis to GitHub pages

1 files changed, 10 insertions, 0 deletions

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