ci: git remote prune origin before git pull

2022-08-23 18:15:28 +08:00 · 2022-08-23 18:15:28 +08:00 · dae7f94152
parent 16dd4a9899
commit dae7f94152
1 changed files with 1 additions and 0 deletions
--- a/1
+++ b/1
@ -53,6 +53,7 @@ def check_docs() {
        }
        sh '''
            cd ${WKC}
+            git remote prune origin
            git pull >/dev/null
            git fetch origin +refs/pull/${CHANGE_ID}/merge
            git checkout -qf FETCH_HEAD