Does any one, in particular @erwint, have any objection if we just completely delete the master branch?

It seems to me that after #123 and #143 and #176 (#179) having a master branch is more confusing than useful, so to make it easier for future contributors to find their way around this project, why not just delete it? (Just for history, it's currently at d8d98ae from today, previous was 5f21765 from 2 years, 3 months ago).

We could wait until https://git.eclipse.org/r/#/c/132982/ (re. #157) is merged.