From 37107ee81f97b8f20107dcc5ee9d83458ecba737 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Gabriel=20N=C3=BCtzi?= <gnuetzi@gmail.com>
Date: Fri, 5 Jul 2024 11:41:44 +0200
Subject: [PATCH] fix: setting Git user/email address

---
 tools/ci/before-script.sh | 2 ++
 tools/general.sh          | 5 +++++
 2 files changed, 7 insertions(+)

diff --git a/tools/ci/before-script.sh b/tools/ci/before-script.sh
index cd8cf80..5d2b1ea 100755
--- a/tools/ci/before-script.sh
+++ b/tools/ci/before-script.sh
@@ -14,4 +14,6 @@ ROOT_DIR=$(git rev-parse --show-toplevel)
 print_info "Current dir: '$(pwd)'"
 print_info "Running as user: $(id)"
 
+ci_setup_git
+
 unset ROOT_DIR
diff --git a/tools/general.sh b/tools/general.sh
index 8e82f7d..068bcd7 100755
--- a/tools/general.sh
+++ b/tools/general.sh
@@ -61,6 +61,11 @@ function ci_is_release() {
     return 1
 }
 
+function ci_setup_git() {
+    git config --global user.name "SDSC CI"
+    git config --global user.email "ci@sdsc.ethz.ch"
+}
+
 function ci_setup_nix() {
     local install_prefix="${1:-/usr/sbin}"