Lukas Diekmann

Turns out this is a bit more complicated. It actually has nothing to do with shrinking (I don't know why I thought it did). Since the box gets entirely removed...

Yes, we used to do something like that, but that leaves us with loads of boxes with trailing whitespaces and we conciously made the decision to exclude them. Because most...

Hmm, that might work. I reason about that for a bit.

I'll probably just do both.

Agreed. My suggestion would be to always try to copy some (partial) subtree if possible and fall back to copying terminals otherwise. Another thing we need to remember is that...

The type would be none and then the incremental lexer will take care of finding a type if possible. E.g. half of `somevariable` would still be an `identifier`. In most...

TODO: - [ ] copy node: clones node - [ ] copy partial node: create new node with partial text and None type - [ ] copy multiple nodes: find...

The bad request on your `wget` example is normal. Why Github does the same I don't know. I'd need some more information. Like your config, if you are using a...

@christopherreay Sorry for the late reply. Do you still have this issue? `SECRET=None` should be fine. Did you set a secret in the Github webhook?

I've been using an organizational hook for years now and haven't had any issues. I wonder if they changed the ping event, because I'm fairly sure this used to work....