Skip to content
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

Position information overhaul #3049

Merged
merged 13 commits into from Mar 12, 2023
Merged

Position information overhaul #3049

merged 13 commits into from Mar 12, 2023

Conversation

jwiesler
Copy link
Contributor

@jwiesler jwiesler commented Feb 28, 2023 •
edited

Blocking on #3034. There are some usages in the PrettyPrinter I won't fix since it's deleted there.

Artiweb

@jwiesler jwiesler self-assigned this Feb 28, 2023
mattulbrich
mattulbrich approved these changes Mar 9, 2023
View reviewed changes
Copy link
Member

@mattulbrich mattulbrich left a comment

Choose a reason for hiding this comment

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

Approved after discussion. Thanks!

@mattulbrich
Copy link
Member

We should use this PR to substantially test our reporting both regarding locations and positions and the issue dialog.

@jwiesler jwiesler enabled auto-merge March 10, 2023 12:54
@jwiesler jwiesler added this pull request to the merge queue Mar 11, 2023
Merged via the queue into KeYProject:main with commit 08c08a6 Mar 12, 2023
@jwiesler jwiesler deleted the positions branch March 12, 2023 01:03
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@mattulbrich mattulbrich mattulbrich approved these changes

Assignees

@jwiesler jwiesler

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
2 participants
@jwiesler @mattulbrich