From 97e9aad483ec6d1932160e8b63d88f7d83422daf Mon Sep 17 00:00:00 2001
From: Oliver Sander <sander@igpm.rwth-aachen.de>
Date: Wed, 19 Feb 2014 15:02:45 +0100
Subject: [PATCH] Remove text file empty.txt

Which is not empty, but contains the text "Leave this file here!".
The file was placed there in 1995, never touched, and is not apparently
referenced from anywhere else.  So out it goes...
---
 lib/empty.txt | 1 -
 1 file changed, 1 deletion(-)
 delete mode 100755 lib/empty.txt

diff --git a/lib/empty.txt b/lib/empty.txt
deleted file mode 100755
index 5855dbe72..000000000
--- a/lib/empty.txt
+++ /dev/null
@@ -1 +0,0 @@
-Leave this file here !
\ No newline at end of file
-- 
GitLab