Skip to content

Commit

Permalink
Better hover markdown separator
Browse files Browse the repository at this point in the history
  • Loading branch information
dlesbre committed Nov 29, 2023
1 parent f48e7ff commit 4d742f7
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion language-server/language/hover.ml
Original file line number Diff line number Diff line change
Expand Up @@ -224,7 +224,7 @@ let ref_info env _sigma ref udecl =
let path = Libnames.pr_path (Nametab.path_of_global ref) ++ canonical_name_info ref in
let args = print_arguments ref in
let args = if Pp.ismt args then [] else ["**Args:** " ^ (Pp.string_of_ppcmds (print_arguments ref))] in
String.concat "\n" @@ [md_code_block @@ compactify @@ Pp.string_of_ppcmds typ]@args@
String.concat "\n\n---\n\n" @@ [md_code_block @@ compactify @@ Pp.string_of_ppcmds typ]@args@
[Format.sprintf "**%s** %s" (pr_globref_kind ref) (Pp.string_of_ppcmds path)]

let mod_info mp =
Expand Down

0 comments on commit 4d742f7

Please sign in to comment.