Closed junghans closed 6 months ago
@G-071 what is the build failure?
The build failures were unrelated. We simply needed to adapt our Jenkins pipelines to a few changes (see #474 ).
The changes in this PR here seem simple enough -- though for completion’s sake I will wait with merging it until #474 is merged first, and the updated tests pass here as well.
@junghans thanks. I will merge it once the tests passed.