Merge build 14 into master

Jenkinsfile

@@ -114,7 +114,7 @@ pipeline {
             passwordVariable: 'GITEA_TOKEN')]) {
             script {
                 sh '''
-                  git fetch origin
+                  git fetch --tags origin
                   git checkout -B gitea-mirror-$BUILD_NUMBER origin/master
                   git rm -f Jenkinsfile
                   git commit -m "Remove Jenkinsfile for Gitea mirror" || echo "No changes to commit"
@@ -129,6 +129,14 @@ pipeline {
                       push master --delete "$branch"
                     fi
                   done
+                  git -c credential.helper="!f() { echo username=${GITEA_USER}; echo password=${GITEA_TOKEN}; }; f" \
+                  push master --tags
+                  git ls-remote --tags master | awk '{print $2}' | sed 's#refs/tags/##' | cut -d'^' -f1 | sort -u | while read tag; do
+                    if [ -n "$tag" ] && ! git show-ref --tags --verify --quiet "refs/tags/$tag"; then
+                      git -c credential.helper="!f() { echo username=${GITEA_USER}; echo password=${GITEA_TOKEN}; }; f" \
+                      push master ":refs/tags/$tag"
+                    fi
+                  done
                   '''
           }
         }