diff options
author | Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-09-30 09:50:48 +0200 |
---|---|---|
committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-09-30 10:54:42 +0200 |
commit | 627659dd1449d4521132efb1f01ad57b128b235c (patch) | |
tree | c1f143c75e5adbfb6e1e702bca5462d64e54344c /plugins/firstorder/rules.mli | |
parent | 1b2d1628dfa52e6c1a5a0c328b80829b03cea58f (diff) |
Give name to warning added in (fdfcdc): arguments-ignore-rename-nonimpl
Diffstat (limited to 'plugins/firstorder/rules.mli')
0 files changed, 0 insertions, 0 deletions