From 3c33272a8217c07f582d056be20eb3725d700376 Mon Sep 17 00:00:00 2001
From: jakubgs <jakubgs@users.noreply.github.com>
Date: Wed, 30 Jun 2021 21:19:34 +0000
Subject: [PATCH] deploy: d1c65a8d06c31f540f905ef1785d7e8bdef483b5

---
 ci/Jenkinsfile.prs | 1 +
 1 file changed, 1 insertion(+)

diff --git a/ci/Jenkinsfile.prs b/ci/Jenkinsfile.prs
index 59b92e679..c56cd929e 100644
--- a/ci/Jenkinsfile.prs
+++ b/ci/Jenkinsfile.prs
@@ -75,6 +75,7 @@ pipeline {
   post {
     success { script { github.notifyPR(true) } }
     failure { script { github.notifyPR(false) } }
+    always { cleanWs() }
   } // post
 } // pipeline