mirror of
https://github.com/jenkinsci/jenkins.git
synced 2026-11-07 09:06:03 +00:00
As I mentioned in the comment, I doubt if this makes any behaviour change, but this seems like a sensible defensive measure that wouldn't hurt.