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.

Sign up for GitHub

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

Jump to bottom

rename start.t -> rev.t #1330

Merged

christian-schilling merged 1 commit into josh-project:master from RalfJung:test-name

May 11, 2024

Contributor

RalfJung commented May 11, 2024

I think an earlier version of rev(...) was called start and probably it was forgotten to rename the test file when the filter got renamed.


          rename start.t -> rev.t

1e4d38f

christian-schilling approved these changes

View reviewed changes

christian-schilling merged commit b28d490 into josh-project:master

1 check passed

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet