*/ $lang['mizar_work_dir'] = 'Mizar work directory (includes subdirectories like TEXT, DICT, and PREL)'; $lang['mizar_share_dir'] = 'Mizar shared files directory'; $lang['mizar_exe_dir'] = 'Mizar executables directory';