From 3f257364c50236d4b062d21e34f8c3c7aac07f29 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 27 Sep 2019 08:52:08 +0200
Subject: [PATCH] [Override Std] Shorter option
---
src/plugins/override_std/options.ml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/plugins/override_std/options.ml b/src/plugins/override_std/options.ml
index 77011bea940..92381aa5eca 100644
--- a/src/plugins/override_std/options.ml
+++ b/src/plugins/override_std/options.ml
@@ -32,7 +32,7 @@ include Plugin.Register
module Enabled = False
(struct
- let option_name = "-override-std-perform"
+ let option_name = "-override-std"
let help = ""
end)
--
GitLab