Skip to content

CI: Temporarily pin tectonic=0.15#4604

Merged
seisman merged 2 commits intomainfrom
ci/pin-tectonic
Apr 28, 2026
Merged

CI: Temporarily pin tectonic=0.15#4604
seisman merged 2 commits intomainfrom
ci/pin-tectonic

Conversation

@seisman
Copy link
Copy Markdown
Member

@seisman seisman commented Apr 28, 2026

Building the PDF documentation started to fail recently with tectonic=0.16 (released two weeks ago), and has been working well with tectonic=0.15 (released in 2024).

xref:

It's likely related to the upstream issue tectonic-typesetting/tectonic#1342.

This PR pins tectonic to 0.15, so that we can have docs updated in CI. I'll open a separate PR to unpin it to track if any future releases fix the issue.

@seisman seisman added maintenance Boring but important stuff for the core devs skip-changelog Skip adding Pull Request to changelog final review call This PR requires final review and approval from a second reviewer labels Apr 28, 2026
@seisman seisman added this to the 0.19.0 milestone Apr 28, 2026
@seisman seisman removed the final review call This PR requires final review and approval from a second reviewer label Apr 28, 2026
@seisman seisman merged commit ebb6ea2 into main Apr 28, 2026
9 checks passed
@seisman seisman deleted the ci/pin-tectonic branch April 28, 2026 10:51
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

maintenance Boring but important stuff for the core devs skip-changelog Skip adding Pull Request to changelog

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants