diff options
author | Erich Eckner <git@eckner.net> | 2020-10-18 10:04:57 +0200 |
---|---|---|
committer | Erich Eckner <git@eckner.net> | 2020-10-18 10:04:57 +0200 |
commit | 12ae1ba84d190c70043892a999b89d817bcb0ce0 (patch) | |
tree | 84d81c0f60b5e0198169b77467488925c0967252 /clean-compile-mpost.in | |
parent | 770473bf1c6dd6e79db50fcd0efa608265bd6d67 (diff) | |
download | clean-compile-mpost-12ae1ba84d190c70043892a999b89d817bcb0ce0.tar.xz |
Diffstat (limited to 'clean-compile-mpost.in')
-rwxr-xr-x | clean-compile-mpost.in | 45 |
1 files changed, 45 insertions, 0 deletions
diff --git a/clean-compile-mpost.in b/clean-compile-mpost.in new file mode 100755 index 0000000..d304f92 --- /dev/null +++ b/clean-compile-mpost.in @@ -0,0 +1,45 @@ +#!#SHELL# + +# Version #VERSION# + +# 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}/" '{}' + |