Makefile newHEADv0.0master

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}/" '{}' +