Join GitHub today
GitHub is home to over 40 million developers working together to host and review code, manage projects, and build software together.Sign up
tectonic: 0.1.9 -> 0.1.11 #51640
Motivation for this change
Yeah, a backport would be appreciated. I can make a PR for one, if wanted.
What do you mean by "both"?