From b2af7187d96d3f28fe91380df14da40c5d55611f Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Thu, 8 Aug 2019 09:04:37 +0200
Subject: [PATCH] we don't clutter the src/ dir any more

---
 src/.gitignore | 46 ----------------------------------------------
 1 file changed, 46 deletions(-)
 delete mode 100644 src/.gitignore

diff --git a/src/.gitignore b/src/.gitignore
deleted file mode 100644
index f1b36f58580..00000000000
--- a/src/.gitignore
+++ /dev/null
@@ -1,46 +0,0 @@
-*.a
-*.aux
-*.bc
-*.boot
-*.bz2
-*.cmi
-*.cmo
-*.cmx
-*.cp
-*.cps
-*.d
-*.dSYM
-*.def
-*.diff
-*.dll
-*.dylib
-*.elc
-*.epub
-*.exe
-*.fn
-*.html
-*.kdev4
-*.ky
-*.ll
-*.llvm
-*.log
-*.o
-*.orig
-*.out
-*.patch
-*.pdb
-*.pdf
-*.pg
-*.pot
-*.pyc
-*.rej
-*.rlib
-*.rustc
-*.so
-*.swo
-*.swp
-*.tmp
-*.toc
-*.tp
-*.vr
-*.x86