From 37b2e6a2c8932f31b8fa2cea80a5560272ce92da Mon Sep 17 00:00:00 2001
From: Harrison Deng <yunyangdeng@gmail.com>
Date: Sun, 9 Jan 2022 01:07:17 -0600
Subject: [PATCH] Added tag pushing.

---
 Jenkinsfile | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Jenkinsfile b/Jenkinsfile
index 070e9c6..b14ab45 100644
--- a/Jenkinsfile
+++ b/Jenkinsfile
@@ -36,6 +36,7 @@ pipeline {
                 sh 'git commit -am "Automatically merged delta branch to master." || exit 0'
                 sshagent(['2e60e630-b240-4c78-87ce-cb2c33d70180']) {
                     sh 'git push origin master'
+                    sh 'git push origin --tags'
                 }
             }
         }