New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Replace usages of `priorities`, `require`, and `import` #16

Merged

rv-jenkins merged 1 commit into master from syntax-cleanup

Feb 22, 2024

Contributor

Scott-Guest commented Feb 21, 2024

Part of runtimeverification/k#4009

Replace usages of deprecated tokens:

syntax priorities with syntax priority
require with requires
import with imports


          Replace deprecated tokens

7ffe2d6

Scott-Guest self-assigned this

Scott-Guest marked this pull request as ready for review

February 21, 2024 23:37

Scott-Guest requested review from gtrepta and Baltoli

February 21, 2024 23:37

Baltoli approved these changes

View reviewed changes

Baltoli added the automerge label

rv-jenkins merged commit dcf27c5 into master

1 check passed

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels