Dirk f16ed46e76 Provide the correct branch to Dockerhub builds ...

... and at the same time allow correct local builds --
the default branch is 3.1dev at the moment.

It still clones the repo from github which isn't
needed. A pure copy command would be the best. However
it might cause other problems.

See also #1559

2020-05-08 11:32:39 +02:00

411 B

Raw Blame History

View Raw