From ec5b4b9a9eef0003c0d39a54489f975fd9bbcd46 Mon Sep 17 00:00:00 2001
From: Andreas Molzer <andreas.molzer@gmx.de>
Date: Fri, 11 Sep 2020 23:27:46 +0200
Subject: [PATCH] Remove a Pipfile?

This slipped through in some merge but I it shouldn't be necessary for
anything? Probably committed/not ignored on accident.
---
 Pipfile | 11 -----------
 1 file changed, 11 deletions(-)
 delete mode 100644 Pipfile

diff --git a/Pipfile b/Pipfile
deleted file mode 100644
index b723d01..0000000
--- a/Pipfile
+++ /dev/null
@@ -1,11 +0,0 @@
-[[source]]
-name = "pypi"
-url = "https://pypi.org/simple"
-verify_ssl = true
-
-[dev-packages]
-
-[packages]
-
-[requires]
-python_version = "3.7"