Skip to content

Actually require compilation ID#138

Merged
gnidan merged 1 commit intomainfrom
compilation-id
Feb 13, 2025
Merged

Actually require compilation ID#138
gnidan merged 1 commit intomainfrom
compilation-id

Conversation

@gnidan
Copy link
Member

@gnidan gnidan commented Feb 13, 2025

Oops this was left out of #131

@gnidan gnidan merged commit 985aa7e into main Feb 13, 2025
3 checks passed
@gnidan gnidan deleted the compilation-id branch February 13, 2025 03:35
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