From 07cf73b393dfbf618aa7ab4ffc91155ca45391d0 Mon Sep 17 00:00:00 2001
From: Vincent Brison <vincent.brison@proton.ch>
Date: Mon, 22 Nov 2021 16:53:32 +0100
Subject: [PATCH] Don't trigger CI when pushing updated release commit

---
 util/commitRelease | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/util/commitRelease b/util/commitRelease
index ab4cb5c6c..02eba7a23 100755
--- a/util/commitRelease
+++ b/util/commitRelease
@@ -40,7 +40,7 @@ EOT
   git status;
 
   git commit -m "[release] $(cat ./new_releases.tmp)"
-  git push origin master;
+  git push origin master -o ci.skip;
 }
 
 main