version 1.129, 2020/05/16 16:26:34 |
version 1.130, 2020/05/16 16:30:59 |
|
|
"bottom." |
"bottom." |
}, |
}, |
|
|
{ .name = "xterm-keys", |
{ .name = "xterm-keys", /* no longer used */ |
.type = OPTIONS_TABLE_FLAG, |
.type = OPTIONS_TABLE_FLAG, |
.scope = OPTIONS_TABLE_WINDOW, |
.scope = OPTIONS_TABLE_WINDOW, |
.default_num = 1, |
.default_num = 1, |
.text = "Whether xterm-style function key sequences should be sent." |
.text = "Whether xterm-style function key sequences should be sent. " |
|
"This option is no longer used." |
}, |
}, |
|
|
/* Hook options. */ |
/* Hook options. */ |