Skip to content

Update pdflatex command for nonstop mode#933

Merged
james-d-mitchell merged 1 commit into
mainfrom
james-d-mitchell-patch-1
May 19, 2026
Merged

Update pdflatex command for nonstop mode#933
james-d-mitchell merged 1 commit into
mainfrom
james-d-mitchell-patch-1

Conversation

@james-d-mitchell
Copy link
Copy Markdown
Member

@james-d-mitchell james-d-mitchell commented May 19, 2026

Suggested by Mark Kambites.

@codecov
Copy link
Copy Markdown

codecov Bot commented May 19, 2026

Codecov Report

❌ Patch coverage is 0% with 2 lines in your changes missing coverage. Please review.
✅ Project coverage is 97.45%. Comparing base (0fe44fd) to head (c5bcb5f).
⚠️ Report is 1 commits behind head on main.

Files with missing lines Patch % Lines
gap/display.gi 0.00% 2 Missing ⚠️
Additional details and impacted files
@@            Coverage Diff             @@
##             main     #933      +/-   ##
==========================================
- Coverage   97.45%   97.45%   -0.01%     
==========================================
  Files          50       50              
  Lines       21188    21189       +1     
  Branches      639      639              
==========================================
  Hits        20649    20649              
- Misses        474      475       +1     
  Partials       65       65              

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:
  • ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.

@james-d-mitchell james-d-mitchell force-pushed the james-d-mitchell-patch-1 branch from 123cdc2 to c5bcb5f Compare May 19, 2026 11:40
@james-d-mitchell james-d-mitchell added the backport-to-stable Label for PRs merged into main that should be cherry-picked onto stable too label May 19, 2026
@james-d-mitchell james-d-mitchell merged commit 585921b into main May 19, 2026
31 checks passed
@james-d-mitchell james-d-mitchell deleted the james-d-mitchell-patch-1 branch May 19, 2026 13:28
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

backport-to-stable Label for PRs merged into main that should be cherry-picked onto stable too

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant