Barak A. Pearlmutter Mon, 19 Dec 2016 13:36:34 -0800
Just remove it in git (unfortunately immediately after uploading 16.1, sorry). But next time, feel free to just push a change! The repo is in collab-maint for a reason.
