Fix old_pins (though it is not used)
[saartuer.git] / .gitignore
2013-10-02 Ralf JungAdd .gitignore