modification script lancement

docker-entrypoint.sh

@@ -8,11 +8,11 @@ id_node=$(id -u node)
 if [ $id_node != ${USER_ID} ]; then
 	if [ -z ${GROUPE_ID} ]; then
 	    echo "Création de l'utilisateur giref avec uid=${USER_ID}"
-	    adduser -u ${USER_ID} -h /home/giref/ -s /bin/bash -D giref;
+	    adduser -u ${USER_ID} -h /home/giref/ -s /bin/bash -D giref
 	else
 	    echo "Création de l'utilisateur giref avec uid=${USER_ID} dans le groupe giref avec gid=${GROUPE_ID}"
 	    addgroup -g ${GROUPE_ID} giref
-	    adduser -u ${USER_ID} -G giref -h /home/giref/ -s /bin/bash -D giref;
+	    adduser -u ${USER_ID} -G giref -h /home/giref/ -s /bin/bash -D giref
 	fi
 	user=giref
 else
@@ -28,6 +28,13 @@ if [ -d /home/.ssh ]; then
 	chown -R $user:$user /home/$user/.ssh
 fi
 
+# settings pour theia
+if [ -f /settings.json ]; then
+	mkdir -p /home/$user/.theia
+	cp /settings.json /home/$user/.theia
+	chown -R $user:$user /home/$user/.theia
+fi
+
 # Enfin, reprend le entrypoint donné ici : https://github.com/theia-ide/theia-apps/blob/master/theia-docker/Dockerfile
 echo "Lancement de theia..."
 su $user bash -c "/usr/local/bin/node /home/theia/src-gen/backend/main.js /home/project --hostname=0.0.0.0"