From f2087508a325bd4dae8be54ea3c6111f6b652775 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Sun, 29 Dec 2013 11:12:49 -0500
Subject: Avoid generating .ml files in native compiler.

---
 kernel/nativelibrary.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/nativelibrary.ml')

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)
-- 
cgit v1.2.3