Opened 4 years ago
Last modified 3 years ago
#22040 closed defect
Close GitHub PRs that have been merged — at Version 2
| 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)
Change History (2)
comment:1 by , 4 years ago
comment:2 by , 4 years ago
| Description: | modified (diff) |
|---|
Note:
See TracTickets
for help on using tickets.
Ping