Set up linting before git push

[paulbert]

I'm working on setting up automatic linting before any push to the repository. First thought is to have a pre-push hook, but there is a slight downside that git hooks aren't automatically stored in the repository so everyone would need to run a command to set up the hooks.

That's certainly the simplest solution, though, so I'll be setting this up for the meeting on Wednesday for everyone to take a look at.