Sean Whitton writes ("Bug#935890: Rename "dgit push-source" to "dgit push""):
> You didn't write much :) Is the thought that `dgit push-source` is
> analogous with `git push` and so should occupy the name `dgit push`?
And it is more primary, in the sense that users probably want
push-source rather than push-built.
> On Thu 05 Sep 2019 at 09:46AM +01, Ian Jackson wrote:
> > Is this worth the disruption ?
>
> If what I just wrote is the only reason for doing this, then I'm not
> convinced that it is.
Fair enough. Maybe we should close this bug then.
Ian.
--
Ian Jackson <[email protected]> These opinions are my own.
If I emailed you from an address @fyvzl.net or @evade.org.uk, that is
a private address which bypasses my fierce spamfilter.
