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