function help() { echo -e "\nERROR: ${1}\nYou must provide a file that can be accessed from within the Docker container. This is possible for files that\n\t- Have a path in \${HOME} or\n\t- Have a full file path that begins with one of \"/hosthome/\", \"/opt/lofar2.0/tango/\" or \"/opt/lofar2.0/\".\n\nWhy is that? Because the file will be loaded from within the Docker container and only some of the host's file system directories are mounted in the container." exit -2 } if [ ${#} -eq 1 ]; then file=${1} else help "A file name must be provided." fi # Check if the filename begins with /hosthome/, /opt/lofar2.0/tango or # /opt/lofar2.0/ or if it is in the ${HOME} directory: if [ ${1:0:10} != /hosthome/ -a ${1:0:20} != /opt/lofar2.0/tango/ -a ${1:0:14} != /opt/lofar2.0/ ]; then pushd $(dirname ${file}) >/dev/null full_path=${PWD} popd >/dev/null # Check if the file's directory begins with ${HOME}. Then it can be # accessed via /hosthome. The replacement will then shorten the result. home_replaced=${full_path#${HOME}} if [ ${#home_replaced} -ne ${#full_path} ]; then if [ ! -f ${file} ]; then help "The file \"${1}\" does not exist." fi # The file can be accessed through /hosthome. Modify the parameter. file=/hosthome${home_replaced}/$(basename ${file}) else # The file is in one of the two: /opt/lofar2.0/tango/ /opt/lofar2.0/ # Provide the full path since it is accessible from within the docker # image because both directories are mounted. file=${full_path}/$(basename ${file}) fi fi docker exec -it ${TANGO_CONTAINER_ENV} dsconfig json2tango --write --update ${file}