diff options
| author | Hugo Herbelin | 2014-05-07 08:31:51 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-05-07 08:31:51 +0200 |
| commit | bab2183aa03bd10917b2e1d915083ea8427f5d6c (patch) | |
| tree | 9389145ae11ad6cf4c93f07cf8c00a242ab01096 /dev | |
| parent | 87e9c331253236b58048f0e9f5d4feea7b5fb04d (diff) | |
Removing comment outdated since eta holds in conversion rule (this
answers #3299).
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions