Skip to content

Conversation

@wilfwilson
Copy link
Collaborator

I noticed that #521 removed these two files. @james-d-mitchell says they should indeed not be present in the distro. But I figured it's best to have it as a separate PR because I like making PRs and I haven't made one for a while.

@wilfwilson wilfwilson added minor A label for PRs or issues that are minor in some sense. technical A necessary technical change, not interesting mathematically/feature-wise labels Aug 25, 2025
@wilfwilson wilfwilson merged commit f8a5276 into digraphs:stable-1.10 Aug 25, 2025
27 checks passed
@wilfwilson wilfwilson deleted the remove-dirstamp branch August 25, 2025 09:15
@wilfwilson
Copy link
Collaborator Author

Thanks Wilf, beautiful.

@wilfwilson wilfwilson added the gap-days-summer-2025-koper Label for things we might/will/did work on in Koper, or that arose there label Aug 26, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

gap-days-summer-2025-koper Label for things we might/will/did work on in Koper, or that arose there minor A label for PRs or issues that are minor in some sense. technical A necessary technical change, not interesting mathematically/feature-wise

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant