diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-21 22:12:55 +0200 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-30 17:50:37 +0200 |
commit | 64d663bc7de8bb21ec98c15ae5876f5d1b1f0b34 (patch) | |
tree | 1035797330c69ea00d2883a2a7732a573d345924 /plugins/omega | |
parent | 3440a9fcc0690b66ff57a693b61dd6ccb13582c0 (diff) |
[api] Reintroduce `Names.global_reference` alias
Due to a bad interaction between PRs, the `Names.global_reference`
alias was removed in 8.9, where it should disappear in 8.10.
The original PR #6156 deprecated the alias in `Libnames`.
Diffstat (limited to 'plugins/omega')
0 files changed, 0 insertions, 0 deletions