1 files changed, 28 insertions, 0 deletions
diff --git a/Konzerte/2018_05_26/make-permanently b/Konzerte/2018_05_26/make-permanently
new file mode 100755
index 0000000..087f29e
--- /dev/null
+++ b/Konzerte/2018_05_26/make-permanently
@@ -0,0 +1,28 @@
+#!/bin/bash
+
+while inotifywait -e DELETE_SELF $(
+  find $(
+    sed -n '
+      :a
+        \/\\$/ {
+          N
+          s/\\\n//
+          ta
+        }
+      s/^\S\+: //
+      T
+      y/ /\n/
+      p
+    ' "$(dirname "$0")/Makefile" | \
+      sed -n '
+        s,^\(\(\.\./\)\+.\+\)/[^/]\+$,\1,
+        T
+        s/[^/]*%.*$//
+        \,^\(\.\./\)*$,d
+        p
+      ' | \
+      sort -u | tee /dev/stderr
+    ) -type f
+  ); do
+  make
+done