Merge pull request #14636 from tjhei/jenkins-disable-old

dealii · Jan 4, 2023 · 55812cf · 55812cf
2 parents 84cb874 + 82b29cf
commit 55812cf
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 197 deletions.
diff --git a/Jenkinsfile b/Jenkinsfile
diff --git a/contrib/ci/Jenkinsfile.mark b/contrib/ci/Jenkinsfile.mark