Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Rm remote actions #3819

Merged
merged 1 commit into from
Aug 13, 2022
Merged

Rm remote actions #3819

merged 1 commit into from
Aug 13, 2022

Conversation

parrt
Copy link
Member

@parrt parrt commented Aug 13, 2022

Looks like hosted github actions I'm working and so I'm going to try turning off the remote actions; we can always back this out if necessary and turn them back on. See #3792

@parrt parrt added this to the 4.10.2 milestone Aug 13, 2022
@parrt parrt changed the base branch from master to dev August 13, 2022 22:15
@parrt
Copy link
Member Author

parrt commented Aug 13, 2022

Hmm... I see this running circleci but not the hosted, despite the hosted.yml being there.

@parrt parrt merged commit a2b84ee into antlr:dev Aug 13, 2022
@parrt parrt deleted the rm-remote-actions branch August 13, 2022 22:29
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant