ENH: New tool for copying files into docker container.

tools/copy_into_docker.sh

+#!/bin/bash
+
+# ** header v3.0
+# This file is a part of the CaosDB Project.
+#
+# Copyright (C) 2019 IndiScale GmbH
+#
+# This program is free software: you can redistribute it and/or modify
+# it under the terms of the GNU Affero General Public License as
+# published by the Free Software Foundation, either version 3 of the
+# License, or (at your option) any later version.
+#
+# This program is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+# GNU Affero General Public License for more details.
+#
+# You should have received a copy of the GNU Affero General Public License
+# along with this program. If not, see <https://www.gnu.org/licenses/>.
+#
+# ** end header
+
+# Copy files which are currently edited or debugged to the caosdb server docker container
+
+set -e
+
+# Copy just the publicly accessible files
+core_dir="$(dirname $0)/../src/core"
+container="compose_caosdb-server_1"
+docker_webui_root="/opt/caosdb/git/caosdb-server/caosdb-webui"
+docker_dir="${docker_webui_root}/src/core/"
+
+docker cp "${core_dir}/." "$container:$docker_dir"
+docker exec -ti -w "$docker_webui_root" "$container" make