From 770473bf1c6dd6e79db50fcd0efa608265bd6d67 Mon Sep 17 00:00:00 2001
From: Erich Eckner <git@eckner.net>
Date: Tue, 28 Apr 2020 10:45:25 +0200
Subject: initial commit from nlopc46.ioq.uni-jena.de

---
 clean-compile-mpost | 43 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 43 insertions(+)
 create mode 100755 clean-compile-mpost

diff --git a/clean-compile-mpost b/clean-compile-mpost
new file mode 100755
index 0000000..6eba233
--- /dev/null
+++ b/clean-compile-mpost
@@ -0,0 +1,43 @@
+#!/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}/" '{}' +
-- 
cgit v1.2.3-54-g00ecf