dev/make-distrib.sh · 28ec4d3f0b8dfb99ad76cab2eb68203bd0a8f62c · pub / frama-c

2 years ago

[dev] make-distrib.sh: fixes the distribution of multiple external plugins. · 07e7b61c

David Bühler authored 2 years ago

This is less efficient but circumvents a bug in tar --concatenate
(https://superuser.com/questions/941475/concatenate-multiple-tar-files-in-one-command)

07e7b61c

History

[dev] make-distrib.sh: fixes the distribution of multiple external plugins.

David Bühler authored 2 years ago

This is less efficient but circumvents a bug in tar --concatenate
(https://superuser.com/questions/941475/concatenate-multiple-tar-files-in-one-command)