Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merging this PR despite CI failure. The CI failure concerns building the reference manual, which fails because of change of `basictex` versions. The change has recently been reflected in Homebrew/homebrew-cask#103001, but evidently some brew/cask/basictex/etc. release/synchronization still needs to happen before we get to reap the benefit of this fix.
- Loading branch information