Use ID pit to store mutation results.

uhafner · Oct 17, 2023 · d148082 · d148082
1 parent 3f9ff7e
commit d148082
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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') {