jenkins: Export the public key

Signed-off-by: Michael Tremer <michael.tremer@ipfire.org>

diff --git a/Jenkinsfile b/Jenkinsfile
index 1824c540e01950a0d871cdbf8411e319adcc7641..41419a142266384d012c105a37f5386f42664d6d 100644 (file)
--- a/Jenkinsfile
+++ b/Jenkinsfile
@@ -483,6 +483,10 @@ pipeline {
                                                        }
                                                }
 
+                                               // Export the public key
+                                               sh "gpg --batch --export --armor ${env.GPG_KEY_ID} \
+                                                       > packages/debian/${env.GPG_KEY_ID}.asc"
+
                                                // Remove the GPG key material as soon as possible
                                                sh "rm -rf $GNUPGHOME"