From f94fa8544476845742078bad95b1627cdec6f0bb Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 8 Jan 2013 21:22:45 +0000 Subject: [PATCH] ML API: build system fix --- scripts/mk_util.py | 1 - 1 file changed, 1 deletion(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 503c3dadd..4c39ff13b 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -357,7 +357,6 @@ def check_ml(): rmf('hello.cmo') rmf('hello.cmx') rmf('a.out') - t.__del__() find_ml_lib() find_ocaml_find()