GitLab

(maybe-copy-distfiles-CMD, maybe-copy-distfiles-SH)
(create-tmp-dist-dir): Added to make --distfiles optional.
(dist): Use create-tmp-dist-dir and maybe-copy-distfiles.