Skip to content

fix(engine): expose type of local_ident.id#851

Merged
W95Psp merged 1 commit into
cryspen:mainfrom
paulmure:local-var-id
Oct 7, 2024
Merged

fix(engine): expose type of local_ident.id#851
W95Psp merged 1 commit into
cryspen:mainfrom
paulmure:local-var-id

Conversation

@paulmure
Copy link
Copy Markdown
Contributor

Close #850

@W95Psp W95Psp enabled auto-merge October 7, 2024 06:33
Copy link
Copy Markdown
Contributor

@W95Psp W95Psp left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

As discussed in #850, that looks ok to me, let's merge.

@W95Psp W95Psp added this pull request to the merge queue Oct 7, 2024
Merged via the queue into cryspen:main with commit 5d259aa Oct 7, 2024
@W95Psp W95Psp deleted the local-var-id branch October 7, 2024 06:54
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Engine: local_ident's id type is opaque

2 participants