Jenkins: delete mark job as well, as it is not needed anymore

This is because invidual jobs report there status without having to

be on a node yet.

diff --git a/contrib/ci/Jenkinsfile.mark b/contrib/ci/Jenkinsfile.mark
deleted file mode 100644 (file)
index 78f8e02..0000000
--- a/contrib/ci/Jenkinsfile.mark
+++ /dev/null
@@ -1,63 +0,0 @@
-#!groovy
-
-/*
-
-This Jenkinsfile is used to mark jobs as "pending" as quickly as possible. The
-other longer running jobs only set the status to pending once they start
-running.
-
-See https://jenkins.tjhei.info/job/dealii-mark/ for details.
-
-*/
-
-/*
-Settings to apply inside Jenkins:
-  - discover pull requests (remove branches/master)
-  - Strategy: merged PR
-  - enable "Disable GitHub Multibranch Status Plugin"
-  - trigger build on pull request comment: .* /rebuild.* (without space)
-  - Jenkinsfile: choose contrib/ci/Jenkinsfile.mark
-  - scan: every 4 hours
-  - discard: 5+ items
-  - docker label: small
-*/
-
-pipeline
-{
-  agent
-  {
-    docker
-    {
-      image 'dealii/indent'
-    }
-  }
-
-  post { cleanup { cleanWs() } }
-
-  stages
-  {
-    stage("check")
-    {
-      steps
-      {
-        githubNotify context: 'ready', description: 'please be patient, testers are spinning up...',  status: 'PENDING'
-        sh '''
-               wget -q -O - https://api.github.com/repos/dealii/dealii/issues/${CHANGE_ID}/labels | grep 'ready to test' || \
-               { echo "This commit will only be tested when it has the label 'ready to test'. Trigger a rebuild by adding a comment that contains '/rebuild'..."; exit 1; }
-            '''
-      }
-      post
-      {
-        failure
-        {
-          githubNotify context: 'ready', description: 'need ready to test label and /rebuild',  status: 'PENDING'
-          script
-          {
-            currentBuild.result='NOT_BUILT'
-          }
-        }
-      }
-    }
-
-  }
-}