infra: Remove BRANCHES file.

This was only interesting when severe discipline was required for
managing branches.  The switch to GIT makes this redundant.  Besides,
I've no longer any idea where all the branches might be. ;-)

diff --git a/BRANCHES b/BRANCHES
deleted file mode 100644 (file)
index 1cd9f21..0000000
--- a/BRANCHES
+++ /dev/null
@@ -1,8 +0,0 @@
-General conventions:
-
-For a branch FOO, we have:
-       FOO:root        point at which FOO leaves trunk or parent branch
-       FOO:merge-N     Nth branch merge point
-
-`ec' -- elliptic curve work
-       ec:merge-1      Closed.