Revert "Move wiki pages to github pages (#18497)"

This reverts commit 40eb803de1.
2019-03-25 13:43:46 +01:00
parent 4a1c393894
commit 161b15f9e4
84 changed files with 186 additions and 10477 deletions
--- a/doc.md
+++ b/doc.md
@ -1,8 +0,0 @@
---
-title: Other documents
-root: ..
-permalink: /doc/
---
-{% for p in site.doc %}
-* [{{ p.title }}]({% include link.html url=p.url %})
-{% endfor %}