Thank you, Peter!
(Why did I not see it in the dashboard? Why did I miss the build failure locally? Hmmm...)


seems it’s there at https://jenkins.tei-c.org/job/TEIP5-Test-dev/680/
The build has been kicked off due to your commit but failed, hence the subsequent jobs have not been started at all.