Skip to content

Comments

Format dune file#26

Merged
mbarbin merged 1 commit intomainfrom
format-dune-file
Apr 8, 2025
Merged

Format dune file#26
mbarbin merged 1 commit intomainfrom
format-dune-file

Conversation

@mbarbin
Copy link
Owner

@mbarbin mbarbin commented Apr 7, 2025

Migration from calls to dune format-dune-file in action to the new (format-dune-file) stanza of dune.3.18.

@mbarbin mbarbin force-pushed the format-dune-file branch from 65b1e68 to 4280e67 Compare April 8, 2025 20:54
@mbarbin mbarbin merged commit 8eb5a47 into main Apr 8, 2025
4 checks passed
@mbarbin mbarbin deleted the format-dune-file branch April 8, 2025 21:03
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