From ee3a9b256e2feb2344415e7f68c817fbf19a0e4a Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Tue, 20 Aug 2019 18:24:52 +0200
Subject: [PATCH] [Dive] Reduce default depth to 2
---
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 c0726125a74..a93edff327e 100644
--- a/src/plugins/dive/self.ml
+++ b/src/plugins/dive/self.ml
@@ -48,7 +48,7 @@ module DepthLimit = Int
let option_name = "-dive-depth-limit"
let help = "Build dependencies up to a depth of N."
let arg_name = "N"
- let default = 3
+ let default = 2
end)
module FromFunctionAlarms = Kernel_function_set
--
GitLab