Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix issue with line numbers introduced in 6534384. #511

Merged
merged 1 commit into from
Apr 27, 2024
Merged

Conversation

rmn30
Copy link
Contributor

@rmn30 rmn30 commented Apr 27, 2024

There was a missing call to Lexing.new_line when lexing a line in a doc comment consisting of only ws + "*" + "\n". This caused line number information to get out of sync resulting in bad latex output and (presumably) other issues.

See also #441 .

There was a missing call to Lexing.new_line when lexing a line in a
doc comment consisting of only ws + "*" + "\n". This caused line
number information to get out of sync resulting in bad latex output
and (presumably) other issues.
@rmn30 rmn30 requested a review from Alasdair April 27, 2024 09:40
Copy link

github-actions bot commented Apr 27, 2024

Test Results

    9 files  ±0     20 suites  ±0   0s ⏱️ ±0s
  619 tests ±0    619 ✅ ±0  0 💤 ±0  0 ❌ ±0 
1 984 runs  ±0  1 983 ✅ ±0  1 💤 ±0  0 ❌ ±0 

Results for commit 6be215f. ± Comparison against base commit dab359f.

♻️ This comment has been updated with latest results.

@Alasdair Alasdair merged commit bb50f71 into sail2 Apr 27, 2024
9 checks passed
@Alasdair
Copy link
Collaborator

Thanks!

@Alasdair Alasdair deleted the fix_lno branch May 2, 2024 20:54
@Alasdair Alasdair removed their request for review May 2, 2024 20:54
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants