From dbc468466a696e52fcf0c0d4fea42b7b19af29b5 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 15 Oct 2019 15:17:11 +0200
Subject: [PATCH] [Builtin] Fixes shortname
---
src/plugins/builtin/options.ml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/plugins/builtin/options.ml b/src/plugins/builtin/options.ml
index e21d5a74fb8..f4e7e8b813b 100644
--- a/src/plugins/builtin/options.ml
+++ b/src/plugins/builtin/options.ml
@@ -26,7 +26,7 @@ let shortname = "builtin"
include Plugin.Register
(struct
let name = name
- let shortname = "-" ^ shortname
+ let shortname = shortname
let help = "Overrides standard library functions"
end)
--
GitLab