diff --git a/plugins/python/py_main.ml b/plugins/python/py_main.ml index e3c5f6a3893a679beda7436111b38f8d8923b22a..bd491542a0e7b2afe142c023a516a9ceca807456 100644 --- a/plugins/python/py_main.ml +++ b/plugins/python/py_main.ml @@ -17,7 +17,12 @@ open Stdlib let debug = Debug.register_flag "python" ~desc:"mini-python plugin debug flag" + +(* NO! this will be executed at plugin load, thus +disabling the warning for ALL WHY3 USERS even if they don't +use the python front-end let () = Debug.set_flag Dterm.debug_ignore_unused_var +*) let mk_id ~loc name = { id_str = name; id_lab = []; id_loc = loc }