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 /docs/user | |
| 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 'docs/user')
0 files changed, 0 insertions, 0 deletions