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