dev scripts can not handle merged tickets

[saraedum]

Merging dependencies fails when one of the tickets has already been merged. In
this case the branch field of the ticket does not contain an actual branch but
a commit hash.

CC: @miguelmarco

Component: misc

Author: Julian Rueth

Branch/Commit: 22e0a10

Reviewer: Volker Braun

Issue created by migration from https://trac.sagemath.org/ticket/16124

[saraedum]

Branch: u/saraedum/ticket/16124

[vbraun]

comment:3

It is an intentional feature that you cannot download arbitrary commits (define by SHA1) from remote git servers. Only named branches can be fetched.

---

New commits:

22e0a10

Handle already merged tickets correctly when merging dependencies in the dev scripts.

[vbraun]

Commit: 22e0a10

[rwst]

comment:6

wontfix because of removal of dev scripts, see https://groups.google.com/forum/?hl=en#!topic/sage-devel/JtVWAdvw-3A

[saraedum]

comment:7

I hope you don't mind that I revert your change. But I do not think that the discussion about the dev scripts removal has reached a conclusion yet.

[vbraun]

Reviewer: Volker Braun

[vbraun]

comment:8

Fine with me if you manage to fill in the author name...

[jdemeyer]

Author: Julian Rueth

[vbraun]

Changed branch from u/saraedum/ticket/16124 to 22e0a10