diff --git a/docs/user/header.html b/docs/user/header.html new file mode 100644 index 0000000000..8e2e514424 --- /dev/null +++ b/docs/user/header.html @@ -0,0 +1,8 @@ + + + + + $projectname: $title + + +