From 818275b7249250780ddd5ed021cae64288514270 Mon Sep 17 00:00:00 2001
From: Martin Nowack <m.nowack@imperial.ac.uk>
Date: Fri, 25 Mar 2022 22:57:31 +0000
Subject: Add support to `sudo` if necessary

Instead if executing system-relevant changes directly, use `sudo` on
Ubuntu-based machines.

Simplifies the installation procedure.
---
 scripts/build/common-functions | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'scripts/build/common-functions')

diff --git a/scripts/build/common-functions b/scripts/build/common-functions
index 6d810d73..c964419f 100644
--- a/scripts/build/common-functions
+++ b/scripts/build/common-functions
@@ -30,4 +30,13 @@ function get_git_hash() {
   else
     echo "${commit_id:0:7}"
   fi
+}
+
+function with_sudo() {
+    echo "Checking sudo $@"
+    if [[ $(whoami) != "root" ]]; then
+        sudo "$@"
+    else
+        "$@"
+    fi
 }
\ No newline at end of file
-- 
cgit 1.4.1