Fix again line numbers in HTML

This commit is contained in:
Denis Merigoux 2022-08-16 11:46:20 +02:00
parent a1ebb6715c
commit 2c40802c57
No known key found for this signature in database
GPG Key ID: EE99DCFA365C3EE3
2 changed files with 3 additions and 3 deletions

View File

@ -135,7 +135,7 @@ let pygmentize_code (c : string Marked.pos) (language : C.backend_lang) : string
"style=colorful,anchorlinenos=True,lineanchors=\""
^ String_common.to_ascii (Pos.get_file (Marked.get_mark c))
^ "\",linenos=table,linenostart="
^ string_of_int (Pos.get_start_line (Marked.get_mark c) - 1);
^ string_of_int (Pos.get_start_line (Marked.get_mark c));
"-o";
temp_file_out;
temp_file_in;

View File

@ -631,8 +631,8 @@ code:
metadata_block:
| BEGIN_METADATA option(law_text) code_and_pos = code text = END_CODE {
let (code, pos) = code_and_pos in
(code, (text, pos))
let (code, _) = code_and_pos in
(code, (text, Pos.from_lpos $sloc))
}