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

Update option names #509

Open

keyboardDrummer wants to merge 2 commits into dafny-lang:master from keyboardDrummer:optionNames

Member

keyboardDrummer commented Nov 7, 2024 •

edited

Loading

Fixes #219

Changes

Rename "Language Server Launch Args" to "Dafny Server Arguments"
Rename "Run Args" to "Dafny Run Arguments"

Note: this PR makes all currently configured values for these options be lost, so let's make sure we only have to change the name once.

New look:

Screenshot 2024-11-07 at 13 39 54


          Update option names

41480c5

keyboardDrummer enabled auto-merge (squash)

November 7, 2024 12:47


          Mention project file

2a4a229

keyboardDrummer requested a review from MikaelMayer

November 7, 2024 13:05

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

Labels

None yet