diff options
| author | Matej Kosik | 2015-10-30 16:31:42 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-10 09:35:10 +0100 |
| commit | 73985c85792da06857199311834962f6a417e71c (patch) | |
| tree | bf85ec28a80f0bb491eda08c0040814561e1be19 /plugins | |
| parent | 32d7eb310f348bf4fcc6222de75bc5b423c9787e (diff) | |
ENH: a small remark about Prod1 and Prod2 typing-rules was added
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions