include documentation in public distribution

2017-07-04 11:24:41 +02:00
parent 80a01f2bdb
commit 0a436db00b
352 changed files with 51487 additions and 1 deletions
--- a/doc/html/search/searchdata.js
+++ b/doc/html/search/searchdata.js
@@ -0,0 +1,36 @@
+var indexSectionsWithContent =
+{
+  0: "abcdefghiklmnopqrstuvwxy",
+  1: "de",
+  2: "p",
+  3: "fmp",
+  4: "abcdefghiklmnopqrstuw",
+  5: "abcefhikmnopsuvwxy",
+  6: "a",
+  7: "ipt"
+};
+
+var indexSectionNames =
+{
+  0: "all",
+  1: "classes",
+  2: "namespaces",
+  3: "files",
+  4: "functions",
+  5: "variables",
+  6: "groups",
+  7: "pages"
+};
+
+var indexSectionLabels =
+{
+  0: "All",
+  1: "Data Structures",
+  2: "Namespaces",
+  3: "Files",
+  4: "Functions",
+  5: "Variables",
+  6: "Modules",
+  7: "Pages"
+};
+