diff options
| author | Hugo Herbelin | 2014-10-03 15:21:05 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-10-03 15:21:10 +0200 |
| commit | 9a82982c1eb8cb1d6a61d3d497d669591fb68747 (patch) | |
| tree | 946bacf9494795d8cfb34f633630bdab13feaa76 /dev/include | |
| parent | 29844f673b5af1b0e50efc7b41cf5660d0a37d03 (diff) | |
Fixing #3657 (check that both sides of a "change with" have the same
type, what is necessary condition to ensure that the conversion of
bodies will not raise an anomaly).
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions