1<?php
2
3$lang['navigation_page'] = 'ID of navigation page';
4$lang['pagefloat'] = 'The name of the menu to use as the floating menu on the right. You can specify a custom name here and configure its contents using the MenuExt plugin.';
5$lang['hide_tools'] = 'Hide tools when user is not logged in';
6