From d14808261a0012ca5283c5881772a53b1038ec3a Mon Sep 17 00:00:00 2001
From: Ulli Hafner <ullrich.hafner@gmail.com>
Date: Tue, 17 Oct 2023 14:57:58 +0200
Subject: [PATCH] Use ID pit to store mutation results.

---
 etc/Jenkinsfile.autograding | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/etc/Jenkinsfile.autograding b/etc/Jenkinsfile.autograding
index e192e53a..6aaa25ec 100644
--- a/etc/Jenkinsfile.autograding
+++ b/etc/Jenkinsfile.autograding
@@ -33,7 +33,7 @@ node {
         withMaven(maven: 'mvn-default', mavenLocalRepo: '/var/data/m2repository', mavenOpts: '-Xmx768m -Xms512m') {
             sh "mvn -ntp org.pitest:pitest-maven:mutationCoverage"
         }
-        recordCoverage tools: [[parser: 'PIT']], sourceCodeRetention: 'EVERY_BUILD'
+        recordCoverage tools: [[parser: 'PIT']], id: 'pit', sourceCodeRetention: 'EVERY_BUILD'
     }
 
     stage ('Collect Maven Warnings') {