diff options
| author | Hugo Herbelin | 2014-11-05 16:00:59 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-11-06 19:59:22 +0100 |
| commit | f30d9777fe19c4e7cc0727947474e08668acae8f (patch) | |
| tree | ec7e1a64219fbc252c6aeb60f75fa4be7706bca3 /plugins | |
| parent | ca609f7ea0653a282a81e5d4f9392b1c05a03d8f (diff) | |
Consequence of changing the definition of Nat.shiftl and Nat.shiftr.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions