Felix> Are they contributing much in size to the git repo? They do not contribute much, however they do cluttter the output of commands that list tags/branches
They do complicate history browsing since they sometimes have arcane branching order. I guess the rest of repository size is consumed by pdf/odt documents. Do we still want to keep history for those? For instance, we could drop historic editions of those binary files. Or we could drop the files and replace them with some asciidoc (which is simpler to review and diff Vladimir
