From 5f3db3c97ecf1a57ddd4c87ddecf5680f1a6544b Mon Sep 17 00:00:00 2001
From: Ugo Pattacini <ugo.pattacini@iit.it>
Date: Tue, 17 Oct 2023 18:03:35 +0200
Subject: [PATCH] Make gitpod owner of `/workspace` (#53)

---
 dockerfiles/Dockerfile | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/dockerfiles/Dockerfile b/dockerfiles/Dockerfile
index 7c1d79d..c9287b0 100644
--- a/dockerfiles/Dockerfile
+++ b/dockerfiles/Dockerfile
@@ -115,6 +115,8 @@ RUN chmod +x /usr/bin/start-vnc-session.sh && \
 
 # Make sure specific dirs are owned by gitpod user
 RUN chown -R gitpod.gitpod ${ROBOTOLOGY_SUPERBUILD_INSTALL_DIR}
+RUN mkdir /workspace && \
+    chown -R gitpod.gitpod /workspace
 
 # Manage ports
 EXPOSE 5901 6080 10000/tcp 10000/udp