merge upstream development #110

Merged
muellerr merged 70 commits from mohr/merge-upstream into develop 2022-09-15 18:34:50 +02:00
122 changed files with 663 additions and 1604 deletions
Showing only changes of commit af282c7d3e - Show all commits

View File

@@ -45,7 +45,7 @@ pipeline {
}
stage('Documentation') {
when {
branch 'mohr/documentation_ci'
branch 'development'
}
steps {
dir(DOCDDIR) {