DON'T MERGE: investigate doc-magic problem in PR #750#751

Closed

hendriktews wants to merge 1 commit intoProofGeneral:masterfrom hendriktews:magic-bug

+7-277

Commits on Mar 28, 2024

DON'T MERGE: investigate doc-magic problem in PR ProofGeneral#750
hendriktews
committed