Modify ↓
#22040 closed defect (fixed)
Close GitHub PRs that have been merged
| Reported by: | taylor.smock | Owned by: | team |
|---|---|---|---|
| Priority: | normal | Milestone: | |
| Component: | Git mirror | Version: | |
| Keywords: | Cc: |
Description (last modified by )
I don't have the ability to close some of the GitHub PRs that have been merged.
Specifically
- https://github.com/JOSM/josm/pull/77
- https://github.com/JOSM/josm/pull/93 (if Firefishy doesn't close it first)
Attachments (0)
Change History (5)
comment:1 by , 3 years ago
comment:2 by , 3 years ago
| Description: | modified (diff) |
|---|
comment:3 by , 3 years ago
| Resolution: | → fixed |
|---|---|
| Status: | new → closed |
comment:5 by , 3 years ago
| Component: | Core → Git mirror |
|---|
Note:
See TracTickets
for help on using tickets.
Ping