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