Actually I just noticed that "git clone -b" does take tag names after all - it's just a bit weird because it only accepts their shortened form (so it's ambiguous in a corner case that probably doesn't matter). That means we don't need to change the build manager side.
Actually I just noticed that "git clone -b" does take tag names after all - it's just a bit weird because it only accepts their shortened form (so it's ambiguous in a corner case that probably doesn't matter). That means we don't need to change the build manager side.