diff options
| author | Erich Eckner <git@eckner.net> | 2022-11-14 19:22:43 +0100 |
|---|---|---|
| committer | Erich Eckner <git@eckner.net> | 2022-11-14 19:22:43 +0100 |
| commit | fd1788a5fa18b09b095ddbe89632ab1109b59a2a (patch) | |
| tree | b1ad0d1e52023a37b6ab5c869395871025a9179a | |
| parent | 3fde57dc61cb3e31e2b966d8595f97abaaf69933 (diff) | |
| download | even-more-utils-fd1788a5fa18b09b095ddbe89632ab1109b59a2a.tar.xz | |
make-permanently: run as long as needed
| -rwxr-xr-x | make-permanently.in | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/make-permanently.in b/make-permanently.in index 659517a..786c61c 100755 --- a/make-permanently.in +++ b/make-permanently.in @@ -82,5 +82,7 @@ while true; do ) inotifywait -e DELETE_SELF,CLOSE_WRITE $(find ${watch_files} -type f) || break fi - make "$@" + while make "$@"; do + make -q "$@" && break + done done |