Skip to content

Conversation

@MikaelMayer
Copy link
Member

Fixes #5749

How has this been tested?

The CI should pass.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

@MikaelMayer MikaelMayer enabled auto-merge (squash) September 5, 2024 20:38
@MikaelMayer MikaelMayer disabled auto-merge September 5, 2024 21:45
@MikaelMayer MikaelMayer changed the title CHore: Removal of debug line for better mergeability Chore: Removal of debug line for better mergeability Sep 5, 2024
@MikaelMayer MikaelMayer enabled auto-merge (squash) September 5, 2024 21:45
@MikaelMayer MikaelMayer merged commit 1845b42 into master Sep 6, 2024
@MikaelMayer MikaelMayer deleted the chore-no-line-debug branch September 6, 2024 15:17
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.

Dafny-generated files are not mergeable due to hard-coded line number debugging info

2 participants