added dir for dev manual and style guide. github pages repo now under doc/html

2026-05-30 03:27:33 +08:00 · 2012-01-19 13:41:49 +01:00
parent cddea3426d
commit 187941d420
5 changed files with 255 additions and 16 deletions
@@ -1,5 +1,5 @@
 # ignore html dir for github pages
-/html
+/doc/html

 *.so
 *.[oa]