Skip to content

Add missing dune-glob dependency#250

Merged
filipeom merged 1 commit intomainfrom
missing-dep
Nov 24, 2024
Merged

Add missing dune-glob dependency#250
filipeom merged 1 commit intomainfrom
missing-dep

Conversation

@filipeom
Copy link
Member

No description provided.

@filipeom filipeom force-pushed the missing-dep branch 2 times, most recently from a57b29a to 07ca819 Compare November 24, 2024 16:28
@filipeom filipeom enabled auto-merge (rebase) November 24, 2024 17:48
@filipeom filipeom merged commit 2f430ed into main Nov 24, 2024
@filipeom filipeom deleted the missing-dep branch November 24, 2024 18:08
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