Skip to content

Update Dependabot label for dependencies#121

Merged
4ever2 merged 1 commit into
mainfrom
4ever2-patch-1
Jul 10, 2026
Merged

Update Dependabot label for dependencies#121
4ever2 merged 1 commit into
mainfrom
4ever2-patch-1

Conversation

@4ever2

@4ever2 4ever2 commented Jul 10, 2026

Copy link
Copy Markdown
Collaborator

No description provided.

@4ever2 4ever2 added the part: infrastructure Issues and PRs related to CI, makefile, opam, dune, scripts, etc. label Jul 10, 2026
@4ever2
4ever2 merged commit 3740774 into main Jul 10, 2026
13 of 14 checks passed
@4ever2
4ever2 deleted the 4ever2-patch-1 branch July 10, 2026 12:06
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

part: infrastructure Issues and PRs related to CI, makefile, opam, dune, scripts, etc.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant