diff options
| author | Pierre-Marie Pédrot | 2019-02-21 13:29:44 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-02-21 13:29:44 +0100 |
| commit | 87b4657566d5d4f0ea3d40dae7ba470d957ffe76 (patch) | |
| tree | ef4343e47e70ca0049536fb4d1b77e9fa7b769ee /dev | |
| parent | 2b2af068f6a938405ed7d4d64fd87f176f00d964 (diff) | |
| parent | 647c16764a497b922cc524ba4d956896caa5db5b (diff) | |
Merge PR #9577: [Namegen] Use Global.exists_objlabel in `next_global_ident_away`
Reviewed-by: maximedenes
Reviewed-by: ppedrot
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions