Skip to content

Fix 'choose contract' in parser#3840

Merged
Drodt merged 1 commit into
mainfrom
fix-choose-contract
Jun 17, 2026
Merged

Fix 'choose contract' in parser#3840
Drodt merged 1 commit into
mainfrom
fix-choose-contract

Conversation

@Drodt

@Drodt Drodt commented Jun 17, 2026

Copy link
Copy Markdown
Member

Intended Change

Small follow up to #3822: \chooseContract was left in the ncore grammar and an implicit token was declared. This PR moves that definition to key.core.

Type of pull request

  • Bug fix (non-breaking change which fixes an issue)
  • Other: Grammar

Ensuring quality

Additional information and contact(s)

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.

@Drodt Drodt self-assigned this Jun 17, 2026
@Drodt Drodt added the 🐞 Bug label Jun 17, 2026

@unp1 unp1 left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

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

Thanks

@Drodt Drodt added this pull request to the merge queue Jun 17, 2026
Merged via the queue into main with commit 97844f4 Jun 17, 2026
36 checks passed
@Drodt Drodt deleted the fix-choose-contract branch June 17, 2026 11:43
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants