From 09292437db25600e12a590ea6151784005843f3c Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 8 Jan 2013 21:02:44 +0000 Subject: [PATCH] ML API: build system fixes Signed-off-by: Christoph M. Wintersteiger --- scripts/mk_util.py | 1 + 1 file changed, 1 insertion(+) 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()