From 1a7a041fb8432fc1d2b490e20b8bc18525a950fe Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Wed, 28 Aug 2019 12:41:00 +0200
Subject: [PATCH] [Dive] Fix warnings during compilation
---
src/plugins/dive/server_interface.ml | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/plugins/dive/server_interface.ml b/src/plugins/dive/server_interface.ml
index 07044b5697a..23cebe7468d 100644
--- a/src/plugins/dive/server_interface.ml
+++ b/src/plugins/dive/server_interface.ml
@@ -65,11 +65,11 @@ module Variable = Data.Collection (struct
let syntax = R.syntax
- let fun_field = R.option "fun"
+ let _fun_field = R.option "fun"
~descr:(Markdown.rm "owner function for a local variable")
(module Data.Jstring)
- let var_field = R.field "var"
+ let _var_field = R.field "var"
~descr:(Markdown.rm "variable name")
(module Data.Jstring)
--
GitLab