diff --git a/_assets/ci/Jenkinsfile.desktop b/_assets/ci/Jenkinsfile.desktop
index c7e460c8468..4d65edb7c98 100644
--- a/_assets/ci/Jenkinsfile.desktop
+++ b/_assets/ci/Jenkinsfile.desktop
@@ -110,18 +110,14 @@ pipeline {
             }
         }
     }
-    stage('Cleanup') {
-        steps {
-            script {
-                cleanTmp()
-                }
-            }
-        }
 } // stages
   post {
      success { script { github.notifyPR(true) } }
      failure { script { github.notifyPR(false) } }
-     cleanup { cleanWs() }
+     cleanup {
+       cleanWs()
+       cleanTmp()
+     }
   } // post
 } // pipeline
 
@@ -158,9 +154,7 @@ def shell(cmd) {
 }
 
 def cleanTmp() {
-    if (env.PLATFORM == 'windows') {
-        sh "rm -rf ${env.WORKSPACE}@tmp"
-    } else {
+    if (env.PLATFORM != 'windows') {
         dir("${env.WORKSPACE}@tmp") { deleteDir() }
     }
-}
\ No newline at end of file
+}