I think this is fixed with both r1892841, r1892845 merged but I am still slightly unsure about when things appear as "tags" in Travis and when as "branches", so it might need further tweaks.
Regards, Joe
I think this is fixed with both r1892841, r1892845 merged but I am still slightly unsure about when things appear as "tags" in Travis and when as "branches", so it might need further tweaks.
Regards, Joe