From 748a2255eb959fac7cf8dc64d9bcd05f5f801cde Mon Sep 17 00:00:00 2001
From: pedro <git2021@cas.cat>
Date: Tue, 24 Sep 2024 12:21:03 -0300
Subject: [PATCH] deploy workbench: bugfix copy of settings.ini

---
 deploy-workbench.sh | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/deploy-workbench.sh b/deploy-workbench.sh
index 3ba88ee..a49f092 100755
--- a/deploy-workbench.sh
+++ b/deploy-workbench.sh
@@ -199,7 +199,12 @@ create_persistence_partition() {
                 mkdir -p "${tmp_rw_mount}"
                 ${SUDO} mount "$(pwd)/${rw_img_path}" "${tmp_rw_mount}"
                 ${SUDO} mkdir -p "${tmp_rw_mount}/settings"
-                ${SUDO} cp -v settings.ini "${tmp_rw_mount}/settings/settings.ini"
+                if [ -f "settings.ini" ]; then
+                        ${SUDO} cp -v settings.ini "${tmp_rw_mount}/settings/settings.ini"
+                else
+                        echo "ERROR: settings.ini does not exist yet, cannot read config from there. You can take inspiration with file settings.ini.example"
+                        exit 1
+                fi
                 ${SUDO} umount "${tmp_rw_mount}"
 
                 uuid="$(blkid "${rw_img_path}" | awk '{ print $3; }')"