Join GitHub today
GitHub is home to over 28 million developers working together to host and review code, manage projects, and build software together.Sign up
Various small fixes #18
this patchset fixes some minor cosmetic bugs and introduces two new settings.
Any comments/ideas are welcome, feel free to cherry-pick any commits you like