From bbc48781914a2adec6692ce6676d618c004a1290 Mon Sep 17 00:00:00 2001
From: none <none>
Date: Sun, 20 Nov 2022 18:21:12 +0100
Subject: [PATCH] mount directories instead of copying

---
 Dockerfile | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Dockerfile b/Dockerfile
index ee41e99..bf5117c 100644
--- a/Dockerfile
+++ b/Dockerfile
@@ -22,11 +22,11 @@ RUN echo 'PS1="\u:\wΣ "' >> /home/user/.bashrc
 # setup workspace
 RUN mkdir -p  /home/user/catkin_ws/src
 WORKDIR /home/user/catkin_ws/src
-COPY manipulability_metrics /home/user/catkin_ws/src
+#COPY manipulability_metrics /home/user/catkin_ws/src
 #RUN git clone https://github.com/tecnalia-medical-robotics/manipulability_metrics
 
 # entry script
-COPY scripts/* /home/user/catkin_ws/scripts/
+#COPY scripts/* /home/user/catkin_ws/scripts/
 WORKDIR /home/user/catkin_ws
 USER root
 #RUN chmod u+x /home/user/catkin_ws/scripts/* && chown user: /home/user/catkin_ws/scripts/*
-- 
GitLab