Release 7.1.0#25

pkriens wants to merge 1 commit intomasterbndtools/workspace:masterfrom

7.1bndtools/workspace:7.1Copy head branch name to clipboard