summaryrefslogtreecommitdiff
path: root/compiler/Driver.ml
diff options
context:
space:
mode:
authorSon Ho2023-09-04 00:59:39 +0200
committerSon Ho2023-09-04 00:59:39 +0200
commit3151e373d64f9bce6146a44cd2d3cc64cac84cbf (patch)
tree4526ae6479542c2429c7b673f7d5abfdf6c598ec /compiler/Driver.ml
parent25a741f1d79c537f5da4d21275eabdb1cc73ca89 (diff)
Fix minor issues
Diffstat (limited to '')
-rw-r--r--compiler/Driver.ml4
1 files changed, 3 insertions, 1 deletions
diff --git a/compiler/Driver.ml b/compiler/Driver.ml
index b646a53d..d88962db 100644
--- a/compiler/Driver.ml
+++ b/compiler/Driver.ml
@@ -17,7 +17,9 @@ let log = main_log
let _ =
(* Set up the logging - for now we use default values - TODO: use the
* command-line arguments *)
- (* By setting a level for the main_logger_handler, we filter everything *)
+ (* By setting a level for the main_logger_handler, we filter everything.
+ To have a good trace: one should switch between Info and Debug.
+ *)
Easy_logging.Handlers.set_level main_logger_handler EL.Debug;
main_log#set_level EL.Info;
llbc_of_json_logger#set_level EL.Info;