Fix old_pins (though it is not used)
authorRalf Jung <post@ralfj.de>
Thu, 10 Oct 2013 13:23:00 +0000 (15:23 +0200)
committerRalf Jung <post@ralfj.de>
Thu, 10 Oct 2013 13:23:00 +0000 (15:23 +0200)

No differences found