From da5536134bd327639b4c5a65c51f0d0ff7ed9f0f Mon Sep 17 00:00:00 2001 From: Valentin Perrelle <valentin.perrelle@cea.fr> Date: Tue, 19 Feb 2019 18:42:40 +0100 Subject: [PATCH] [Dive] Fix error message for command line varinfo inputs --- src/plugins/dive/self.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/plugins/dive/self.ml b/src/plugins/dive/self.ml index 87adec5f7ee..3c1c7e782b2 100644 --- a/src/plugins/dive/self.ml +++ b/src/plugins/dive/self.ml @@ -77,7 +77,7 @@ struct try Globals.Vars.find_from_astinfo name VGlobal with Not_found -> - raise (Cannot_build ("no global variable '" ^ name ^ "'")) + raise (Cannot_build ("no global variable '" ^ s ^ "'")) let to_string vi = match Kernel_function.find_defining_kf vi with -- GitLab