diff options
Diffstat (limited to 'clean-compile-mpost')
-rwxr-xr-x | clean-compile-mpost | 43 |
1 files changed, 0 insertions, 43 deletions
diff --git a/clean-compile-mpost b/clean-compile-mpost deleted file mode 100755 index 6eba233..0000000 --- a/clean-compile-mpost +++ /dev/null @@ -1,43 +0,0 @@ -#!/bin/bash - -# clean-compile-mpost source.mp target-dir/ additional-file1 additional-file2 ... - -if ! source=$(readlink -e "$1"); then - >&2 printf 'Cannot read source "%s"\n' "$1" - exit 1 -fi -shift -if [ $# -eq 0 ]; then - target_dir=$(pwd) -else - if ! target_dir=$(readlink -e "$1"); then - >&2 printf 'Cannot read target-dir "%s"\n' "$1" - exit 1 - fi - shift -fi -if ! [ -d "${target_dir}" ]; then - >&2 printf 'Target-dir "%s" is no directory\n' "${target_dir}" - exit 1 -fi - -tmp_dir=$(mktemp -d) -trap 'cd /; rm -rf --one-file-system "${tmp_dir}"' EXIT - -for additional_file in "$@"; do - if ! cp "${additional_file}" "${tmp_dir}/"; then - >&2 printf 'Cannot not copy "%s"\n' "${additional_file}" - exit 1 - fi -done -if ! cp "${source}" "${tmp_dir}/"; then - >&2 printf 'Cannot not copy "%s"\n' "${additional_file}" - exit 1 -fi - -cd "${tmp_dir}" -mpost "${source##*/}" || exit $? -find . \ - -type f \ - -name "*.mps" \ - -exec install -m644 -t "${target_dir}/" '{}' + |