Merge branch 'gh-pages' into devel

2026-09-20 14:38:18 +08:00 · 2018-06-09 20:43:00 -07:00
parent 44817a8095 c9bd43f61c
commit 8ad0703d4f
29 changed files with 1830 additions and 407 deletions
@@ -5,6 +5,9 @@
 		},
 		{
 			"path": "tools"
+		},
+		{
+			"path": "docs"
 		}
 	],
 	"settings": {
@@ -44,4 +47,4 @@
 			"future": "cpp"
 		}
 	}
-}
+}