Bug#935890: Rename "dgit push-source" to "dgit push"

[Sean Whitton]

Hello,

On Thu 05 Sep 2019 at 04:54PM +01, Ian Jackson wrote:

> Fair enough.  Maybe we should close this bug then.

We might just leave it open to see if any users think this is a good
idea.

-- 
Sean Whitton

signature.asc
Description: PGP signature