options: remove 'guiheadroom'

This commit is contained in:
Justin M. Keyes
2017-04-04 03:38:57 +02:00
parent e348e256f3
commit a7f34e1991
5 changed files with 0 additions and 62 deletions

View File

@@ -1025,13 +1025,6 @@ return {
redraw={'everything'},
enable_if=false,
},
{
full_name='guiheadroom', abbreviation='ghr',
type='number', scope={'global'},
vi_def=true,
enable_if=false,
defaults={if_true={vi=50}}
},
{
full_name='guioptions', abbreviation='go',
type='string', list='flags', scope={'global'},