diff --git a/scripts/mk_util.py b/scripts/mk_util.py index c1f899f6d..75e2af52d 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -355,7 +355,6 @@ def check_ml(): os.remove('hello.cmi') os.remove('hello.cmo') os.remove('hello.cmx') - os.remove('hello.obj') os.remove('a.out') find_ml_lib()