From dd42b45467d3fb01e62065964ed7f402a0ba1cb8 Mon Sep 17 00:00:00 2001
From: Carl Hetherington <cth@carlh.net>
Date: Thu, 27 Jul 2017 13:14:32 +0100
Subject: [PATCH] Missing file.

---
 .gitignore           |  1 +
 doc/manual/config.py | 24 ++++++++++++++++++++++++
 2 files changed, 25 insertions(+)
 create mode 100644 doc/manual/config.py

diff --git a/.gitignore b/.gitignore
index 5f1da95e1..6e0786af5 100644
--- a/.gitignore
+++ b/.gitignore
@@ -13,6 +13,7 @@ sync
 doc/manual/html
 doc/manual/pdf
 doc/manual/extensions.ent
+doc/manual/config.xml
 doc/design/*.pdf
 doc/design/*.log
 doc/design/*.aux
diff --git a/doc/manual/config.py b/doc/manual/config.py
new file mode 100644
index 000000000..673174bf2
--- /dev/null
+++ b/doc/manual/config.py
@@ -0,0 +1,24 @@
+import sys
+current_tag = None
+current_doc = None
+current_opt = False
+print '<itemizedlist>'
+with open(sys.argv[1]) as f:
+    for line in f:
+        line = line.strip();
+        if line.startswith('/* [XML'):
+            code = line.split()[1]
+            current_tag = line.split()[2]
+            current_opt = code == '[XML:opt]'
+            line = line[5+len(code)+len(current_tag):]
+            current_doc = ''
+        if current_tag is not None:
+            current_doc += line.replace('/* [XML] ', '').replace('*/', '').strip() + ' '
+        if line.find('*/') != -1 and current_tag is not None:
+            if current_opt:
+                optional = ' (optional)'
+            else:
+                optional = ''
+            print '<listitem><code>&lt;%s&gt;</code>%s &#8212; %s</listitem>' % (current_tag, optional, current_doc.strip())
+            current_tag = None
+print '</itemizedlist>'
-- 
2.30.2