diff --git a/doc/header.html b/doc/header.html index 5ea4bb59..23e998e6 100644 --- a/doc/header.html +++ b/doc/header.html @@ -91,6 +91,40 @@ } + $treeview $search