From 93d1c5d3f9fb9150b1a5ac27f60b2b7978bc9dc3 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Wed, 11 Dec 2019 18:07:49 +0100
Subject: [PATCH] [Server] Better name for the service.
---
src/plugins/server/kernel_project.ml | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/plugins/server/kernel_project.ml b/src/plugins/server/kernel_project.ml
index 052bc13e3f8..2982af38085 100644
--- a/src/plugins/server/kernel_project.ml
+++ b/src/plugins/server/kernel_project.ml
@@ -127,8 +127,8 @@ let () = Request.register ~page
let () =
Request.register
~kind:`GET
- ~page ~name:"kernel.project.getSourceFiles"
- ~descr:(Md.plain "Get the files of the current project")
+ ~page ~name:"kernel.project.getSourceFileNames"
+ ~descr:(Md.plain "Get the source file names of the current project")
~input:(module Junit) ~output:(module Jstring.Jlist)
Kernel.Files.get
--
GitLab