Author: joseph Date: 2015-08-20 10:13:02 +0200 (Thu, 20 Aug 2015) New Revision: 5875 Removed: tags/V2000-08-05/ Log: Remove second ancient tag Both this and the previous commit tidy up stuff from many years ago: they showed up in the (new) Git mirror and are pretty useless.