Skip to content

Comments

Try to die if no operators defined#562

Merged
FCO merged 1 commit intomasterfrom
die-if-no-operators
Dec 19, 2022
Merged

Try to die if no operators defined#562
FCO merged 1 commit intomasterfrom
die-if-no-operators

Conversation

@FCO
Copy link
Owner

@FCO FCO commented Dec 17, 2022

WiP

@FCO FCO force-pushed the die-if-no-operators branch 2 times, most recently from 5174ef8 to 40659b8 Compare December 18, 2022 02:04
@FCO FCO changed the title WiP: Try to die if no operators defined Try to die if no operators defined Dec 18, 2022
@FCO FCO force-pushed the die-if-no-operators branch from 40659b8 to 8495446 Compare December 18, 2022 02:31
@FCO FCO merged commit 5834e51 into master Dec 19, 2022
@FCO FCO deleted the die-if-no-operators branch December 19, 2022 21:13
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