From 80a79336f2d2e701fdaee28e2ae7c895bf7d2e1f Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 7 Nov 2018 09:30:32 +0100
Subject: [PATCH] chore(.gitignore): ignore library/Makefile

---
 .gitignore | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.gitignore b/.gitignore
index 7c23483281..09700a2fdc 100644
--- a/.gitignore
+++ b/.gitignore
@@ -24,3 +24,4 @@ settings.json
 /library/init/version.lean
 CMakeSettings.json
 CppProperties.json
+/library/Makefile