diff options
author | 2017-03-17 20:27:44 +0100 | |
---|---|---|
committer | 2017-03-21 15:51:53 +0100 | |
commit | aa9e94275ccac92311a6bdac563b61a6c7876cec (patch) | |
tree | e220e1469c7d1b3c8dbefdd806f809cfb6a2ac12 /tactics | |
parent | fb04bc5cae0d648c379b9eb44f8b515f8e15b854 (diff) |
[ide protocol] Add comment about leftover parameter.
We try to address @silene 's concerns, which indeed are legitimate.
Diffstat (limited to 'tactics')
0 files changed, 0 insertions, 0 deletions