From ed0fa9324592293e97f8a0da267cc3eb384a1e03 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 19 Jan 2015 17:35:19 +0000 Subject: [PATCH] Minor adjustments after rebase Signed-off-by: Christoph M. Wintersteiger --- examples/ml/ml_example.ml | 2 +- scripts/mk_util.py | 15 ++++----------- 2 files changed, 5 insertions(+), 12 deletions(-) diff --git a/examples/ml/ml_example.ml b/examples/ml/ml_example.ml index 25862b2d7..33334930e 100644 --- a/examples/ml/ml_example.ml +++ b/examples/ml/ml_example.ml @@ -190,7 +190,7 @@ let basic_tests ( ctx : context ) = (* Error handling test. *) try ( let i = Integer.mk_numeral_s ctx "1/2" in - raise (TestFailedException "") (* unreachable *) + raise (TestFailedException (to_string i)) (* unreachable *) ) with Z3native.Exception(_) -> ( Printf.printf "Exception caught, OK.\n" diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 49ff79824..30c305047 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -357,14 +357,13 @@ def check_ml(): rmf('hello.cmo') rmf('hello.cmx') rmf('a.out') - rmf('hello.o') find_ml_lib() find_ocaml_find() def find_ocaml_find(): global OCAMLFIND if is_verbose(): - print ('Testing %s...' % OCAMLFIND) + print ("Testing %s..." % OCAMLFIND) r = exec_cmd([OCAMLFIND, 'printconf']) if r != 0: OCAMLFIND='' @@ -1743,7 +1742,6 @@ def mk_config(): if is_java_enabled(): print('JNI Bindings: %s' % JNI_HOME) print('Java Compiler: %s' % JAVAC) - print('ML API: %s' % is_ml_enabled()) if is_ml_enabled(): print('OCaml Compiler: %s' % OCAMLC) print('OCaml Native: %s' % OCAMLOPT) @@ -1866,11 +1864,10 @@ def mk_config(): if is_java_enabled(): print('JNI Bindings: %s' % JNI_HOME) print('Java Compiler: %s' % JAVAC) - print('ML API: %s' % is_ml_enabled()) if is_ml_enabled(): - print('Ocaml Compiler: %s' % OCAMLC) - print('Ocaml Native: %s' % OCAMLOPT) - print('Ocaml Library: %s' % OCAML_LIB) + print('OCaml Compiler: %s' % OCAMLC) + print('OCaml Native: %s' % OCAMLOPT) + print('OCaml Library: %s' % OCAML_LIB) def mk_install(out): out.write('install: ') @@ -2437,9 +2434,6 @@ def mk_bindings(api_files): if is_java_enabled(): check_java() mk_z3consts_java(api_files) - if is_ml_enabled(): - check_ml() - mk_z3consts_ml(api_files) _execfile(os.path.join('scripts', 'update_api.py'), g) # HACK cp_z3py_to_build() if is_ml_enabled(): @@ -2808,7 +2802,6 @@ def mk_z3consts_ml(api_files): decls[words[1]] = idx idx = idx + 1 linenum = linenum + 1 - efile.write('end\n') if VERBOSE: print ('Generated "%s/z3enums.ml"' % ('%s' % gendir)) efile = open('%s.mli' % os.path.join(gendir, "z3enums"), 'w')