summaryrefslogtreecommitdiff
path: root/compiler/Config.ml
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--compiler/Config.ml5
1 files changed, 5 insertions, 0 deletions
diff --git a/compiler/Config.ml b/compiler/Config.ml
index ce9b0e0c..bfb9d161 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -162,6 +162,11 @@ let backward_no_state_update = ref false
*)
let split_files = ref true
+(** For Lean, controls whether we generate a lakefile or not.
+
+ *)
+let lean_gen_lakefile = ref false
+
(** If true, treat the unit functions (function taking no inputs and returning
no outputs) as unit tests: evaluate them with the interpreter and check that
they don't panic.