diff options
| author | Mateusz Kowalczyk <fuuzetsu@fuuzetsu.co.uk> | 2014-08-24 15:14:23 +0100 |
|---|---|---|
| committer | Mateusz Kowalczyk <fuuzetsu@fuuzetsu.co.uk> | 2014-08-24 15:14:23 +0100 |
| commit | be7b1003893947c96dfa50b1bbd5281541f81949 (patch) | |
| tree | 7604f22a32124351e27eaa50dd82a4998802a6ac /CHANGES | |
| parent | fe15219565c9fd4e5ed919a1987021438911c197 (diff) | |
Delete few unused/irrelevant/badly-place files.
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 3 |
1 files changed, 3 insertions, 0 deletions
@@ -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) |