diff options
| author | Maxime Dénès | 2013-12-29 11:12:49 -0500 |
|---|---|---|
| committer | Maxime Dénès | 2013-12-29 11:12:49 -0500 |
| commit | f2087508a325bd4dae8be54ea3c6111f6b652775 (patch) | |
| tree | c1878e087daf15e96594be0e78d15182f2ca5d08 /kernel/nativelibrary.ml | |
| parent | 381b2c6e77cd204aa143192a5a65e8832ae0633b (diff) | |
Avoid generating .ml files in native compiler.
Diffstat (limited to 'kernel/nativelibrary.ml')
| -rw-r--r-- | kernel/nativelibrary.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml index 39717c351c..6418ac4504 100644 --- a/kernel/nativelibrary.ml +++ b/kernel/nativelibrary.ml @@ -57,6 +57,6 @@ let dump_library mp dp env mod_expr = let compile_library dir code load_path f = let header = mk_library_header dir in - let ml_filename = f^".ml" in + let ml_filename = f^".native" in write_ml_code ml_filename ~header code; fst (call_compiler ml_filename load_path) |