changeset 31480 | 05937d6aafb5 |
parent 31312 | 1c00e4ff3c99 |
child 32738 | 15bb09ca0378 |
--- a/src/Pure/ML-Systems/compiler_polyml-5.2.ML Sat Jun 06 21:46:36 2009 +0200 +++ b/src/Pure/ML-Systems/compiler_polyml-5.2.ML Sat Jun 06 21:47:02 2009 +0200 @@ -38,7 +38,7 @@ PolyML.compiler (get, parameters) ()) handle exn => (put ("Exception- " ^ General.exnMessage exn ^ " raised"); - error (output ()); raise exn); + error (output ()); reraise exn); in if verbose then print (output ()) else () end; fun use_file context verbose name =