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

Fix legacy option for citation in `MANUAL.txt` #9114

Merged

jgm merged 1 commit into jgm:main from 3w36zj6:main

Oct 1, 2023

Contributor

3w36zj6 commented Oct 1, 2023


          Fix legacy option for citation

2807b74

jgm merged commit 33cdce8 into jgm:main

1 of 4 checks passed

Owner

jgm commented Oct 1, 2023

thanks!

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

Labels

None yet