diff --git a/tools/reproduce_comparison/Jenkinsfile b/tools/reproduce_comparison/Jenkinsfile
index 2a2053871..4004d9b5f 100644
--- a/tools/reproduce_comparison/Jenkinsfile
+++ b/tools/reproduce_comparison/Jenkinsfile
@@ -141,6 +141,7 @@ pipeline {
                             } else {
                                 echo 'Success: two builds are the same!'
                             }
+                            archiveArtifacts artifacts: "**/repro_diff.out"
                         }
                     } catch (Exception err) {
                         echo err.getMessage()