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

texinfo manuals: fix obsolete @inforef #725

Merged
merged 1 commit into from
Jan 17, 2024

Conversation

hendriktews
Copy link
Collaborator

@hendriktews hendriktews commented Jan 16, 2024

In most cases, this is a simple replacement, using @pxref in most cases.

Closes #721

In most cases, this is a simple replacement, using @pxref in most
cases.
@erikmd
Copy link
Member

erikmd commented Jan 16, 2024

Thanks!

I'm not texinfo-savvy enough to review this, but looks good at first sight.

@hendriktews I'd also say: Please go ahead if you're confident in this doc fix! — and just check the online doc (automatically-deployed from master) afterwards:

@hendriktews
Copy link
Collaborator Author

I checked the info version carefully at each modification.

@hendriktews hendriktews merged commit 43285bd into ProofGeneral:master Jan 17, 2024
119 checks passed
@hendriktews hendriktews deleted the inforef branch January 17, 2024 21:12
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

Successfully merging this pull request may close these issues.

makeinfo reports warning: @inforef is obsolete
2 participants