diff options
| author | Enrico Lumetti <enrico.lumetti@gmail.com> | 2016-08-25 02:14:50 +0200 |
|---|---|---|
| committer | Enrico Lumetti <enrico.lumetti@gmail.com> | 2016-08-25 02:14:50 +0200 |
| commit | ddff67da39b2a4c578ecc6d5a46e4d1d7bfd213b (patch) | |
| tree | e5f12cd097ce5608befb32924a28fb6087b7c64b | |
| parent | 9124851029700026bc937c81da829fbadcc5b29d (diff) | |
Name JSON resize parameters explicitely
| -rw-r--r-- | doc/json_ui.asciidoc | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/json_ui.asciidoc b/doc/json_ui.asciidoc index 87980df3..4cc7f611 100644 --- a/doc/json_ui.asciidoc +++ b/doc/json_ui.asciidoc @@ -44,4 +44,4 @@ Here are the requests that can be written by the json ui on stdout: The requests that the json ui can interpret on stdin are: * keys(String key1, String key2...): keystrokes -* resize(int x, int y): notify ui resize +* resize(int rows, int columns): notify ui resize |