Skip to content

remove current dir prefix when printing positions#1404

Merged
fblanqui merged 2 commits into
Deducteam:masterfrom
fblanqui:pos
Jun 10, 2026
Merged

remove current dir prefix when printing positions#1404
fblanqui merged 2 commits into
Deducteam:masterfrom
fblanqui:pos

Conversation

@fblanqui

Copy link
Copy Markdown
Member

No description provided.

@fblanqui fblanqui merged commit 892d549 into Deducteam:master Jun 10, 2026
23 checks passed
@fblanqui fblanqui deleted the pos branch June 10, 2026 11:54
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.

1 participant