diff options
| author | mergify[bot] | 2022-06-22 02:01:31 +0000 |
|---|---|---|
| committer | GitHub | 2022-06-22 02:01:31 +0000 |
| commit | 7e67ca1ef93e53d4b9b6f8e13a21d69e0c5daac4 (patch) | |
| tree | 86cffa0bb07590835426df7664510d5515502c61 /plugin | |
| parent | cea238bb9f6cb364d0c6c6229ff316eebc8224ec (diff) | |
Pass optional name in ImportDefinitionAnno (#2592) (#2594)
Used for separate elaboration of Definition and Instance
(cherry picked from commit 48d57cc8db6f38fdf0e23b7dce36caa404c871b8)
Co-authored-by: Girish Pai <girish.pai@sifive.com>
Diffstat (limited to 'plugin')
0 files changed, 0 insertions, 0 deletions
