Skip to content

Arguably resyntax shouldn't need to run each time I edit the OP #1302

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

Closed
Lazerbeak12345 opened this issue Feb 2, 2023 · 4 comments
Closed

Comments

@Lazerbeak12345
Copy link
Contributor

          Arguably resyntax shouldn't need to run each time I edit the OP

Originally posted by @Lazerbeak12345 in #1300 (comment)

@samth
Copy link
Member

samth commented Feb 2, 2023

I don't understand how else it would work. If the diff changes, then resyntax either re-runs or is out of date. Can you explain more about what you're suggesting?

@shhyou
Copy link
Contributor

shhyou commented Feb 2, 2023

I think @Lazerbeak12345 didn't push any new diff but just edited their comment in the thread

@Lazerbeak12345
Copy link
Contributor Author

I think @Lazerbeak12345 didn't push any new diff but just edited their comment in the thread

Yes. This exactly

@shhyou
Copy link
Contributor

shhyou commented Feb 19, 2023

@Lazerbeak12345 said:

          Arguably resyntax shouldn't need to run each time I edit the OP

@Lazerbeak12345 I think you only need to remove this line

The synchronize event:
https://docs.github.com/en/webhooks-and-events/webhooks/webhook-events-and-payloads?actionType=synchronize#pull_request

A pull request's head branch was updated. For example, the head branch was updated from the base branch or new commits were pushed to the head branch.

The edited event:
https://docs.github.com/en/webhooks-and-events/webhooks/webhook-events-and-payloads?actionType=edited#pull_request:

The title or body of a pull request was edited.

capfredf added a commit to capfredf/typed-racket that referenced this issue Feb 19, 2023
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

No branches or pull requests

3 participants