From 9c36ddc5e2babc093e3ab1e8982d8b7bc7f0c213 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Mon, 7 Dec 2020 17:04:27 +0100
Subject: [PATCH] [server] Add source location to marker info.
---
src/plugins/server/kernel_ast.ml | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml
index a3fe97c94e4..53b973e8883 100644
--- a/src/plugins/server/kernel_ast.ml
+++ b/src/plugins/server/kernel_ast.ml
@@ -196,8 +196,8 @@ struct
in
let () =
States.column
- ~name:"position"
- ~descr:(Md.plain "Marker position")
+ ~name:"loc"
+ ~descr:(Md.plain "Source location")
~data:(module Kernel_main.LogSource)
~get:(fun (tag, _) -> fst (Printer_tag.loc_of_localizable tag))
model
--
GitLab