Move wiki pages to github pages (#18497)

2019-03-21 10:35:00 +01:00
parent 02c039f102
commit 40eb803de1
83 changed files with 10461 additions and 186 deletions
--- a/doc.md
+++ b/doc.md
@ -0,0 +1,7 @@
+---
+title: Other documents
+---
+
+{% for p in site.doc %}
+* [{{ p.title }}]({% include link.html url=p.url %})
+{% endfor %}