Felipe Contreras [off-list ref] writes:

+"${args[@]}" -o "$out" "$1" ||
+{ rm -f "$out"; false; }

It would be so nice if this worked, but here is what I saw in a
quick-and-dirty experiment:

    $ f () { echo foo >"$1" && sleep 20 && echo bar >>"$1"; }
    $ f hoi ;# wait sufficiently long
    $ cat hoi
    foo
    bar
    $ f hoi ;# wait a bit and hit ^C
    ^C
    $ cat hoi
    foo
    $ rm hoi
    $ f hoi || rm hoi ;# wait a bit and hit ^C
    ^C
    $ cat hoi
    foo

So, I suspect it unfortunately may not work well.

We need to get 2/8 redone without bash-ism, but it would not affect
the correctness of this step, I would think, whether this is done in
bash or implemented in a plain vanilla POSIX shell.

Thanks.