From be7b1003893947c96dfa50b1bbd5281541f81949 Mon Sep 17 00:00:00 2001
From: Mateusz Kowalczyk <fuuzetsu@fuuzetsu.co.uk>
Date: Sun, 24 Aug 2014 15:14:23 +0100
Subject: Delete few unused/irrelevant/badly-place files.

---
 CHANGES | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 7214e48e..a8155673 100644
--- a/CHANGES
+++ b/CHANGES
@@ -25,6 +25,9 @@ Changes in version 2.15.0
 
  * Omit unnecessary ‘forall’s (#315 and #86)
 
+ * Remove some files which were really old or did not belong in the
+   repository in the first place.
+
 Changes in version 2.14.3
 
  * Fix parsing of identifiers with ^ or ⋆ in them (#298)
-- 
cgit v1.2.3