diff options
author | Aleksey Kladov <[email protected]> | 2020-10-20 14:38:11 +0100 |
---|---|---|
committer | Aleksey Kladov <[email protected]> | 2020-10-20 14:38:11 +0100 |
commit | af4e75533f2c071330e740e2fa94b131e3a2b538 (patch) | |
tree | 6f517a43814751d8b1ea478b5ed03baf57b4f0b5 /.github/actions/github-release/main.js | |
parent | be762ccccd5a86632e60351518528d078785a3e2 (diff) |
Rename declaration_name -> display_name
Declaration names sounds like a name of declaration -- something you
can use for analysis. It empathically isn't, and is just a label
displayed in various UI. It's important not to confuse the two, least
we accidentally mix semantics with UI (I believe, there's already a
case of this in the FamousDefs at least).
Diffstat (limited to '.github/actions/github-release/main.js')
0 files changed, 0 insertions, 0 deletions