From 6027282baebbe55f2beb3e5299b8ca1ad8680d54 Mon Sep 17 00:00:00 2001
From: Thierry Parmentelat <thierry.parmentelat@inria.fr>
Date: Thu, 14 Jan 2016 13:49:58 +0100
Subject: [PATCH] missing

---
 website/index.py | 45 +++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 45 insertions(+)
 create mode 100755 website/index.py

diff --git a/website/index.py b/website/index.py
new file mode 100755
index 00000000..fe137e55
--- /dev/null
+++ b/website/index.py
@@ -0,0 +1,45 @@
+#!/usr/bin/env python3
+# -*- coding: utf-8 -*-
+
+# computes an index file in markdown/index.md from ./index.md with all the other md files referenced
+
+import sys
+import os
+from glob import glob
+
+source = "index.md"
+output_dir = "markdown"
+
+index_line_format = " * [{title}]({base}.html)\n"
+
+TITLE="title:"
+
+def get_title(filename):
+    with open(filename) as input:
+        for line in input:
+            if line.startswith(TITLE):
+                return line[len(TITLE):].strip()
+    return filename
+
+def main():
+    if not os.path.isfile(source):
+        print("Source not found {}".format(source))
+        sys.exit(1)
+
+    output = os.path.join(output_dir, source)
+    with open(output, 'w') as result:
+        # copy index.md
+        with open(source) as input:
+            result.write(input.read())
+        for other in sys.argv[1:]:
+            dir = os.path.dirname(other) or "."
+            base = os.path.basename(other).replace(".md", "")
+            title = get_title(other)
+            # skip index from the index...
+            if base == "index":
+                continue
+            # menu generated
+            #result.write(index_line_format.format(**locals()))
+    print("(Over)wrote {}".format(output))
+
+main()
-- 
2.43.0