MAINT, FIX: [ci skip] tag is ignored by azure.

[massich]

#5857 timeline shows that azure ignored the [ci skip] tag in 4a5c543 commit.

@larsoner feel free to take over if you know how to fix it? (otherwise, I'll do it after release)

@drammock do you think we should add a description of the tags. Feel free to push in this PR to reword anything you like.

[larsoner]

We wait for this to be properly resolved

https://developercommunity.visualstudio.com/idea/420289/add-support-ci-skip-and-azure-skip-to-azure-pipeli.html

[larsoner]

(It's fine to say that people should do it this way in the docs even it doesn't work. I'm fairly confident it will soon-ish, so it'll keep people in the practice of doing what will eventually work, and in the meantime just burn a few extra CI cycles we have no other way to skip without manual cancellation, which is a pain and requires privileges.)

[massich]

@drammock change what you fancy and merge when happy.

Thx

[codecov]

Codecov Report

Merging #6317 into master will decrease coverage by 1.77%.
The diff coverage is n/a.

@@            Coverage Diff             @@
##           master    #6317      +/-   ##
==========================================
- Coverage   89.23%   87.45%   -1.78%     
==========================================
  Files         417      417              
  Lines       75180    75179       -1     
  Branches    12377    12377              
==========================================
- Hits        67085    65751    -1334     
- Misses       5217     6575    +1358     
+ Partials     2878     2853      -25

[larsoner]

Looks good:

https://13123-1301584-gh.circle-artifacts.com/0/dev/contributing.html#github-workflow

Thanks @massich @drammock