diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 4c39ff13b..503c3dadd 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -357,6 +357,7 @@ def check_ml(): rmf('hello.cmo') rmf('hello.cmx') rmf('a.out') + t.__del__() find_ml_lib() find_ocaml_find()