From c000941b9fb1e460cbf38e72b360fd0b1743fda6 Mon Sep 17 00:00:00 2001
From: Andrea Dell'Amico <andrea.dellamico@isti.cnr.it>
Date: Sat, 2 Apr 2022 01:52:25 +0200
Subject: [PATCH] Fix the check of a workspace dir inside the home.

---
 06_workspace_mount.sh | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/06_workspace_mount.sh b/06_workspace_mount.sh
index c112ba9..5751a5b 100644
--- a/06_workspace_mount.sh
+++ b/06_workspace_mount.sh
@@ -27,10 +27,12 @@ chown ${USER}:${USER} $workspace_dir
 chown -R ${USER}:${USER} $workspace_logdir
 
 _retval=
-/bin/rm /home/${USER}/workspace
-_retval=$?
+if [ -d /home/${USER}/workspace ]; then
+  rmdir /home/${USER}/workspace
+  _retval=$?
+fi
 if [ $_retval -ne 0 ]; then
-    echo "The user has a directory named 'workspace' inside their home directory"
+    echo "The user has a directory named 'workspace' inside their home directory and it is not empty."
     echo "Not starting the workspace mount"
     exit
 else