Git: ignore a few more nonsource files