I'm a bit confused about the branch system because I haven't been working on smash for a while. Is okay to merge this on master, right? Master is our "develop" and then we have devel_0.12.x etc. Or... where should the things from milestone 0.13.0 go?
Closes #296 (closed)